Solide comme un Rocq : une introduction au vericoding

Les tests et les types sont censés nous protéger des bugs. Mais qui vérifie que ces garanties tiennent vraiment ?

Aujourd’hui, les agents IA écrivent du code plus vite qu’on ne peut le relire. Cette question n’a jamais été aussi urgente.

Le vericoding, c’est l’idée de faire de la vérification formelle un outil du quotidien : sortir les assistants de preuve comme Rocq des labos de recherche pour les mettre entre les mains des équipes qui livrent en prod.

Écrire une preuve, c’est dur. Écrire ce qu’on veut prouver, beaucoup moins. C’est là que l’IA entre en jeu : vous dites ce qui doit être vrai, la machine se débrouille pour démontrer pourquoi. On obtient alors des garanties d’un nouveau genre : des interfaces qui ne sont plus des promesses, mais des contrats prouvés.

On commencera par repérer le code qui mérite d’être prouvé : les invariants, les machines à états, les règles métier où un bug ne se résume pas à un incident mais peut coûter très cher. On verra où la preuve rapporte gros, et où elle ne vaut pas l’effort.

Ensuite, on passera à la pratique : comment livrer du code prouvé. Backend, frontend, systèmes événementiels, jusqu’au firmware embarqué, on verra comment déployer ce code et ce que ça change dans votre archi et votre codebase quand vous savez que ça marche.

On a commencé par douter de nos garanties. On repartira avec des fondations solides comme un Rocq.