Formal Verification in Rocq, an Exhaustive Testing

In this talk, we present formal verification, a technique for mathematically verifying code and ensuring it is safe for any possible inputs.

We explore in particular the theorem prover Rocq, and how we use it to model and verify production code at Formal Land. We show the two primary methods to create a code model, by testing or proving the equivalence with the implementation, and the main classes of properties that are interesting to formally verify on a program.