Formal Verification in Practice: Lessons from Signal's PQC Migration So Far
Rolfe Schmidt (Signal, Research Engineer)
The migration to post-quantum cryptography introduces subtle new challenges: KEMs behave differently from familiar primitives and performance constraints force complex protocol designs all while applications are becoming more feature-rich. This talk presents Signal’s real-world experience with using formal verification tools to navigate these challenges.
Through four concrete stories—from PQXDH key agreement and the Triple Ratchet protocol to secure backups and TEE-backed services—I will show how tools like ProVerif, F*, TLA+, and the Formosa-Crypto toolchain are playing an important role. We will see how they helped us catch subtle binding issues, iteratively design complex protocols, debug concurrent systems, and gain confidence in compiled code.
While Signal is still in the early stages of integrating these tools into our engineering practice, we are already seeing real value. I will argue that the PQC transition not only makes formal verification more important than ever, but also presents an opportunity: by investing in making these tools more usable and accessible, we can fundamentally improve how our community builds secure and reliable systems for decades to come.