Glossary
Vérification formelle
Prouver mathématiquement — et non juste tester — qu'un smart contract satisfait une spécification précise, via des outils comme Certora, K ou des assistants de preuve.
La vérification formelle remplace les tests par la preuve. L'ingénieur écrit une spécification ("l'offre totale égale la somme des soldes", "aucun appelant ne peut retirer plus que son solde") et un outil de vérification prouve que la spec tient pour toute entrée possible, ou bien produit un contre-exemple.
Des outils comme Certora Prover, Halmos, KEVM, et des assistants de preuve dédiés (Coq, Lean, Isabelle) sont utilisés sur les contrats les plus critiques : Maker, Aave, Compound, Lido. Le coût est élevé — écrire la spec correctement est un travail d'ingénierie à part entière — mais pour des contrats à plusieurs milliards, c'est de plus en plus la norme.