这方面的研究最近非常热,IEEE Symposium on Security & Privacy 2019 (S&P'19)发表了一篇Simple High-Level Code For Cryptographic Arithmetic -- With Proofs, Without Compromises,相关github页面 fiat-crypto: Cryptographic Primitive Code Generation by Fiat
之前还有一些研究论文(包括CCS 2017的HACL和今年最新的EverCrypt):
Secure, fast and verified cryptographic applications: a scalable approach
HACL*: A Verified Modern Cryptographic Library
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider
其中EverCrypt号称完成了经过验证、且和其它所有密码算法库实现相比性能最好的Curve25519实现(即使其它密码算法库没有经过验证,例如OpenSSL)