Event

<p>In this talk, we present formal verification, a technique for mathematically verifying code and ensuring it is safe for any possible inputs.</p> <p>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.</p>