$ coqc -Q . FV
// why formal methods?
Formal verification is the act of mathematically proving that a program meets its specification, not testing it on a handful of inputs, but guaranteeing correctness across all possible executions.
I am deeply invested in this field and convinced that the future of computer-science security runs through writing programs in formal languages. As software grows more complex and AI-generated code spreads, stating a property once and getting a machine-checked proof that it holds forever is the strongest assurance we can offer. Rather than patching vulnerabilities after deployment, we prevent them at the source, by making incorrect programs impossible to express.
Testing
finds bugs
Runs the program on chosen inputs. A green suite means "no bug seen yet": the untested paths stay unknown.
Proving
proves their absence
A machine-checked argument covers every input at once. If it type-checks, the property holds, permanently.
// proof-assistants
These systems let you state arbitrary theorems about programs and prove them interactively. They (almost) all share the same pipeline: you write a specification and a proof, a tiny trusted kernel checks it, and then verified code is extracted or compiled out.
They differ mainly in where trust lives. Kernel-checked systems re-verify every proof through a minimal core; SMT-backed systems trade some trust for automation by leaning on an external solver (Z3) that sits inside the trusted base.
// verify --crypto
Cryptography needs two guarantees at once: the maths must be secure (a break implies solving a hard problem) and the implementation must match that maths, in constant time, down to the assembly. No single tool does everything, so they hand off to one another across four layers: from a high-level security model down to the running binary.
An assembly-like language whose compiler is itself proved correct. You get predictable, constant-time machine code with no hidden compiler surprises, ideal for primitives like ChaCha20 or Kyber.
Game-based proofs: it formalises reductions such as "breaking this scheme means solving a hard problem" (IND-CCA2, EUF-CMA), and its extracted model is checked against the Jasmin code.
Works in the computational model and automates the sequence of game transformations, proving whole protocols secure: TLS 1.3, Signal, WireGuard.
Lifts an existing binary through symbolic execution into a sound formal model, so a deployed closed-source library can be fed to CryptoVerif or EasyCrypt for analysis.
// verify --smt <program>
Instead of interactive proofs, these tools verify programs written in mainstream languages (Rust, C…). You annotate the code with contracts; the tool turns the "what could go wrong?" question into logical formulas and hands them to an automated solver. When it succeeds there is no manual proof to write; when it fails you often get a concrete counterexample.
A companion worth noting: Eurydice is not a verifier but a compiler that turns a safe Rust subset (via the same Charon frontend as Aeneas & hax) into readable low-level C, the bridge from Rust-based proofs to embedded and kernel deployment.