2019.03.21 00:59:53 (1108518553374859264) from Daniel J. Bernstein:
Over the past day a quick demo of the #angr binary-analysis toolkit turned into a prototype verifier https://cr.yp.to/2019/unrolldemo-20190319.html checking correctness of Seiler's vectorized NTT asm in Kyber (see https://eprint.iacr.org/2018/039). Shouldn't be hard to generalize to many more linear maps mod q.
2019.12.27 08:39:28 (1210465202967400448) from Daniel J. Bernstein:
Did a few cleanups and updates to recognize optimizations in the latest versions of angr. Same URL.