RT @email@example.com First release of djbsort: super-fast constant-time automatically verified AVX2 sorting code for int32 arrays. https://sorting.cr.yp.to (Next target is ARM NEON.) Verification starts with the #angr toolkit for symbolic execution, which in turn uses libVEX from Valgrind.
The performance numbers here are quite impressive. Some caveats and limitations though, but djb claims they can be mostly overcome with more development effort.