Verified Software: Theories, Tools, and Experiments is a conference that aims to advance the state of the art in software verification.

At VSTTE 2024 in Prague, Karthik spoke about how formal verification can be used to speed up software development and clarify the security of real-world cryptography from design to implementation. In particular, he showed how these techniques are crucial for the post-quantum transition, using examples from our analysis of post-quantum protocols like PQXDH and our verified ML-KEM implementation.

The slides for Karthik’s invited talk are available here.

If you have any questions about how formal methods and verified crypto can help you, send us an email.