# Verification formelle en Solidity : Halmos et Certora
La plupart des tests Solidity repondent a la question "est-ce que ca marche pour les cas que j'ai essayes ?" Le fuzzing elargit cela a "est-ce que ca marche pour des milliers de cas aleatoires ?" La verification formelle pose une question plus forte : "existe-t-il une entree, quelque part, qui casse ma propriete ?" Quand la reponse est non, vous obtenez une preuve mathematique plutot qu'une coche verte. Cet article explique ce que la verification ajoute au fuzzing, comment ecrire des proprietes et des invariants, et comment deux outils concrets, Halmos et le Certora Prover, abordent le probleme.
Ce que la verification formelle ajoute au fuzzing
Un fuzzer comme le moteur integre de Foundry echantillonne des entrees concretes. Il est rapide, peu couteux, et attrape beaucoup de bugs, mais il ne peut explorer qu'une tranche finie de l'espace des entrees. Si une vulnerabilite vit dans une valeur precise d'un uint256, le fuzzer peut ne jamais tomber dessus.
Les outils de verification formelle raisonnent sur toutes les entrees a la fois. Ils le font via l'execution symbolique : au lieu d'executer votre fonction avec le nombre 42, ils l'executent avec une variable symbolique x qui represente chaque valeur possible. L'outil confie ensuite les contraintes logiques resultantes a un solveur SMT (typiquement Z3 ou un backend similaire) et demande : une affectation de x peut-elle violer l'assertion ?
- Si le solveur repond unsat (aucune affectation n'existe), la propriete tient pour toute entree.
- S'il repond sat, il renvoie un contre-exemple concret, une entree precise qui casse la propriete.
Ce contre-exemple est le gain pratique. Vous n'apprenez pas seulement que quelque chose ne va pas ; vous obtenez la transaction exacte qui le prouve.
Le compromis est l'explosion des chemins. Les boucles et les piles d'appels profondes multiplient le nombre de chemins que le solveur doit considerer, donc la plupart des outils sont *bornes* : ils verifient jusqu'a N iterations de boucle ou une profondeur d'appel fixe. Soyez honnete sur cette borne quand vous lisez les resultats.
Proprietes et invariants
La verification ne vaut que la propriete que vous ecrivez. Deux formes dominent.
Les proprietes (parfois appelees regles) decrivent ce qu'un seul appel de fonction doit garantir. Exemple : "apres que transfer(to, amount) reussit, le solde de l'emetteur diminue d'exactement amount."
Les invariants decrivent un fait qui doit tenir dans chaque etat atteignable, avant et apres toute fonction exposee par le contrat. Exemple : "la somme de tous les soldes est toujours egale a totalSupply." Un invariant est l'enonce le plus puissant car il contraint le contrat sur tout son cycle de vie, pas juste un appel.
De bonnes proprietes ont tendance a etre :
Halmos : open source, style Foundry
Halmos, d'a16z, execute vos tests Solidity de style Foundry de maniere symbolique. Si vous ecrivez deja des tests Foundry, la courbe d'apprentissage est faible. La convention est une fonction prefixee par check_ au lieu de test. Chaque parametre de cette fonction devient une valeur symbolique, donc une seule fonction check_ remplace toute une campagne de fuzzing, mais avec une preuve a la fin.
Voici une propriete pour un token minimal, prouvant que transfer deplace exactement amount et ne gonfle jamais l'offre :
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.24;
import {Test} from "forge-std/Test.sol";
import {Token} from "../src/Token.sol";
contract TokenSymbolicTest is Test {
Token internal token;
function setUp() public {
token = new Token();
}
// Chaque parametre ici est symbolique : Halmos explore toutes les valeurs.
function check_transfer(address from, address to, uint256 amount) public {
vm.assume(from != to);
vm.prank(from);
token.mint(from, amount);
uint256 supplyBefore = token.totalSupply();
uint256 fromBefore = token.balanceOf(from);
uint256 toBefore = token.balanceOf(to);
vm.prank(from);
bool ok = token.transfer(to, amount);
if (ok) {
assertEq(token.balanceOf(from), fromBefore - amount);
assertEq(token.balanceOf(to), toBefore + amount);
assertEq(token.totalSupply(), supplyBefore); // l'offre est conservee
}
}
}
Vous le lancez en ligne de commande :
halmos --function check_transferSi la propriete tient, Halmos signale le chemin comme reussi. Sinon, il imprime un contre-exemple avec des valeurs concretes pour from, to et amount. Comme les boucles sont bornees, vous controlez la profondeur explicitement :
halmos --function check_transfer --loop 4L'avantage principal de Halmos est la reutilisation. Vous tirez parti du harnais de test, des cheatcodes (vm.assume, vm.prank) et du modele mental que vous avez deja, et vous transformez un test de fuzzing en preuve bornee en renommant le prefixe et en resserrant les hypotheses.
Certora Prover : des specs dediees en CVL
Le Certora Prover separe la specification du harnais de test. Vous ecrivez les proprietes dans un langage dedie, CVL (Certora Verification Language), stocke dans un fichier .spec a cote du contrat. CVL est concu pour la verification, donc il exprime directement invariants et regles relationnelles, et le Prover n'impose pas les memes bornes de boucle qu'un runner de style Foundry pour de nombreux patterns (les boucles sont quand meme gerees, souvent via un deroulage que vous configurez).
Une regle CVL reflete la propriete ci-dessus :
rule transferPreservesSupply(address to, uint256 amount) {
env e;
require e.msg.sender != to;
uint256 supplyBefore = totalSupply();
uint256 senderBefore = balanceOf(e.msg.sender);
uint256 toBefore = balanceOf(to);
transfer(e, to, amount);
assert totalSupply() == supplyBefore, "l'offre doit etre conservee";
assert balanceOf(e.msg.sender) == senderBefore - amount;
assert balanceOf(to) == toBefore + amount;
}
La ou Certora brille, c'est sur les invariants. Le Prover verifie un invariant en deux etapes : il confirme que le constructeur l'etablit, puis confirme que chaque methode publique le preserve. Vous n'enumerez pas les methodes ; le Prover le fait. Cet exemple enonce que l'offre totale egale la somme de deux soldes suivis et tient sur tout le contrat :
invariant supplyEqualsBalances()
totalSupply() == balanceOf(alice) + balanceOf(bob)
{
preserved {
require alice != bob;
}
}
Le bloc preserved vous permet d'enoncer des hypotheses qui doivent tenir avant chaque methode. Vous pouvez aussi restreindre les fonctions contre lesquelles un invariant est verifie avec une clause filtered, par exemple en ignorant un mint privilegie qui change legitimement l'offre.
Comment choisir
| | Halmos | Certora Prover |
|---|---|---|
| Langage de spec | Solidity (tests check_) | Fichiers .spec CVL |
| Mise en place | Reutilise le harnais Foundry | Spec separee, fichier de config |
| Cout | Open source, gratuit | Commercial, avec acces communautaire |
| Point fort | Preuves bornees rapides, iteration rapide | Invariants profonds sur toutes les methodes |
Les deux sont complementaires plutot que rivaux. Un workflow courant consiste a prototyper les proprietes dans Halmos parce que la boucle de l'idee au resultat est courte, puis a promouvoir les invariants les plus importants vers CVL pour les garanties plus fortes, couvrant toutes les methodes, que le Certora Prover fournit.
Quelques precautions valent pour les deux outils. La verification prouve la propriete que vous avez ecrite, pas celle que vous vouliez dire, donc une spec faible donne une fausse confiance. Les appels externes et les boucles non bornees restent difficiles, et vous devrez souvent les modeliser ou les resumer. Traitez le travail comme iteratif : ecrivez une propriete, obtenez un contre-exemple, affinez, recommencez.
Mettez-le en pratique sur Solingo
Le moyen le plus rapide d'interioriser tout cela est de casser une propriete volontairement et de regarder le contre-exemple apparaitre. Sur app.solingo-blockchain.xyz vous pouvez ecrire un petit token, enoncer un invariant comme la conservation de l'offre, introduire un bug subtil, et voir comment une obligation de preuve echoue la ou un fuzzer serait reste vert. Commencez par un invariant, prouvez-le, puis essayez de le casser.