Using EasyCrypt and Jasmin for post-quantum verification

Cryptographic code is essential for secure communication in various applications, but ensuring its correctness and security can be challenging. Formal verification techniques are used to prove that a piece of code correctly implements a specification. In this blog post, the authors discuss formal verification tools such as EasyCrypt and Jasmin, which help verify cryptographic implementations. They also emphasize the importance of formal verification for post-quantum cryptography, as deploying algorithms with flaws in their security properties could have severe consequences. The authors are working towards a formally verified implementation of FrodoKEM and collaborating to create a library that can be used in real-world connections.