Over the last 10 years or so, using mathematical proof assistants and other formal-logic tools for cryptography code has gone from a relatively new idea to standard practice. I've been lucky enough to have a front-row seat to that transformation, having started doing formal-methods research in 2015 and then switched to a focus on cryptography implementation since 2021. Code from my master's thesis project, "fiat-crypto", is included in every major browser as well as AWS, Cloudflare, Linux, OpenBSD, and standard crypto libraries for Go, Zig, and Rust (RustCrypto, dalek). In addition to verifying code correctness, designers of high-level protocols like Signal's recently announced post-quantum ratchet increasingly use mathematical tools (ProVerif in Signal's case) to check their work.

Despite the growing popularity of these formal techniques and their relevance to personal information security, few people are aware of them, and they maintain a reputation for being hard to learn and esoteric. I'd like to demystify the topic and show examples of how anyone can use proof assistants in small, standalone ways as part of the coding or design process. My hope is that next time a colleague asks for review of a complex high-speed bit-twiddling algorithm, instead of staring at the code line-by-line, attendees of my talk will know they can write a computer-checked proof to confirm or deny that the algorithm achieves its intended result.