In this blog post, we present a short introduction to Rocq, a formal verification system, as a summary of the guide Rocq in a Hurry from Yves Bertot of the Rocq team.
Rocq is the formal system that we use exclusively, but other interactive theorem provers work the same way. From this introduction, you can get a sense of how the verification of mathematical statements or security properties of programs works.