Russell O’Connor joined Brink engineers to explain his work on formal verification of software, the process of mathematically proving that a program satisfies its specification.
In this discussion we covered:
- An overview of formal verification of software
- A walkthrough using a multiplication function in libsecp256k1
- Coq, Rocq, Clightgen
- SafeGCD (formal verification paper)
- Q&A with audience
This discussion was recorded on August 6, 2025.
About Brink
Brink is a Bitcoin research and development centre, founded in 2020 to support independent open source protocol developers and mentor new contributors. If you or your organization is interested in supporting open source Bitcoin development, feel free to email us, donate@brink.dev.
Developers interested in the grant program can apply now.
Keep in touch
Subscribe to the Brink newsletter for future blog posts.