2018.02.08 19:01:47 (961661348848562176) from Daniel J. Bernstein, replying to unknown (961647686264000513):
Verification strategy for this type of sorting code for one input length: symbolically execute the code to build DAG of min-max operations; scan the DAG to find merging networks; verify each merging network using a standard linear-size set of inputs with a completeness theorem.