AutoVerus transforme 40 heures d'écriture de proof en 3 appels LLM. L'astuce consiste à savoir quand abandonner.

La partie la plus difficile de la vérification formelle n’a jamais été le vérificateur. C’est l’écriture du proof.

Donnez à un ingénieur Rust senior Verus, le vérificateur basé sur SMT de Microsoft Research, et il peut annoter une fonction avec des preconditions et des postconditions en une après-midi. Le vérificateur lui dira alors, avec une certitude mécanique, si la fonction satisfait ces contracts pour chaque entrée possible. Cette partie est satisfaisante.

Puis il rencontre une loop. Le vérificateur se plaint de ne pas pouvoir établir la postcondition. L’ingénieur a besoin d’un invariant, une déclaration logique qui est vraie avant et après chaque itération. Trouver cet invariant nécessitait auparavant un doctorat, ou au moins quarante heures de trial and error. AutoVerus, publié à l’OOPSLA 2025, automatise plus de 90% de ce travail en utilisant un réseau d’agents LLM. La tâche de proof médiane se résout en moins de 30 secondes ou trois appels LLM.

Voici comment cela fonctionne réellement, ce que cela vous coûte et où cela casse encore.

Le vrai bottleneck est la recherche d’invariant, pas le solveur SMT

Verus étend Rust avec du ghost code, des preconditions et des postconditions. Vous écrivez quelque chose comme ceci :

use vstd::prelude::*;

verus! {
    fn sum(arr: &[i32]) -> (result: i32)
        requires
            arr.len() <= 0x40000000,
        ensures
            result == spec_sum(arr@),
    {
        let mut total = 0;
        let mut i = 0;
        while i < arr.len()
            invariant
                0 <= i <= arr.len(),
                total == spec_sum(arr@.subrange(0, i as int)),
        {
            total = total + arr[i];
            i = i + 1;
        }
        total
    }
}

La clause requires est la precondition. La clause ensures est la postcondition. Le bloc invariant à l’intérieur de la loop while est ce qui fait avancer le proof. Il dit au solveur SMT ce qui reste vrai à chaque itération.

La partie difficile est l’invariant. total == spec_sum(arr@.subrange(0, i as int)) n’est pas évident. Un humain l’écrit en pensant de manière inductive à ce qui reste vrai après avoir traité les premiers éléments i. AutoVerus génère cela automatiquement en traitant la synthèse d’invariant comme un problème de search guidé par le feedback du vérificateur.

Comment AutoVerus utilise les agents LLM comme stratégie de search

AutoVerus n’est pas un seul prompt vers GPT-4. C’est une pipeline d’agents spécialisés qui se passent du contexte structuré les uns aux autres.

Le premier agent lit votre fonction Rust et ses doc comments. Il extrait les verification conditions et génère un draft initial des clauses requires, ensures et invariant.

Le deuxième agent alimente ces annotations dans Verus. Verus compile le code annoté et demande à son solveur SMT, généralement Z3, de discharger les proof obligations. Si le solveur dit UNSAT, la propriété tient. S’il dit SAT, il produit un counterexample. La plupart du temps, le premier draft échoue.

L’agent de réparation lit le message d’erreur du vérificateur et la proof obligation échouée. Il suggère un invariant plus fort, une bound plus serrée ou un auxiliary lemma. Le cycle se répète : générer, vérifier, réparer. AutoVerus rapporte une convergence médiane de trois appels LLM. Plus de la moitié des 150 tâches de benchmark non triviales se terminent en moins de 30 secondes.

L’idée n’est pas que les LLMs soient brillants en logique. La search de proof est un problème d’optimisation locale, et les LLMs sont assez bons pour deviner des améliorations locales afin de naviguer dans l’espace plus vite qu’un humain tapant à la main.

Ce que signifie réellement le chiffre de 90%

AutoVerus a atteint plus de 90% d’automatisation de proof sur un benchmark de 150 tâches de proof Rust non triviales. Celles-ci incluaient du raisonnement sur les array bounds, de l’accumulation de loop et du traversal de structures récursives. Le benchmark provenait de codebases Verus réelles.

Le chiffre de 90% signifie que la pipeline LLM a généré un proof que Verus a accepté sans intervention humaine. Cela ne signifie pas que la specification est ce que le programmeur avait l’intention de faire. Le LLM infère l’intention à partir des noms de fonction, des doc comments et des type signatures. Si votre fonction s’appelle process et que votre doc comment dit “handles the thing”, la specification générée sera générique et possiblement fausse.

C’est la même division du travail que les copilots ont introduite pour la génération de code. Le LLM écrit le premier draft. L’humain le révise pour la correctness du domaine. La différence est qu’un proof erroné est silencieux. Un proof généré qui passe la vérification peut prouver la mauvaise propriété. Vous avez toujours besoin d’un humain qui comprend ce que la fonction est censée faire.

Ce qu’AutoVerus ne peut pas faire

AutoVerus est limité par ce que Verus peut exprimer. Verus gère un subset de Rust. Il ne supporte pas l’async, les closures ou certaines collections de la standard library. Si votre code spawne des tasks avec tokio, AutoVerus ne peut pas encore vous aider.

AutoVerus est aussi lié aux patterns. Le taux de succès de 90% s’applique au code qui ressemble à la distribution d’entraînement : des loops sur des arrays, de l’accumulation arithmétique, du bounds checking. Si votre proof nécessite un auxiliary lemma non évident, l’agent de réparation peut boucler jusqu’à atteindre sa limite d’itération. À ce moment-là, vous retournez écrire le proof à la main.

Le coût n’est pas non plus nul. Les tâches de benchmark coûtent des cents par proof. Un module complet peut coûter dix à trente dollars en appels API. C’est deux ordres de grandeur moins cher que le temps d’un ingénieur de vérification, mais ce n’est pas gratuit.

Exécuter AutoVerus sur du code réel

AutoVerus est disponible auprès de Microsoft Research. Le dépôt est microsoft/verus-proof-synthesis sur GitHub. Il s’attend à ce que Verus soit installé.

Voici le workflow pratique :

# 1. Install Verus
git clone https://github.com/verus-lang/verus.git
cd verus && source ./source/vstd.sh

# 2. Clone AutoVerus
git clone https://github.com/microsoft/verus-proof-synthesis.git
cd verus-proof-synthesis

# 3. Set your API key for the LLM backend
export OPENAI_API_KEY="sk-..."

# 4. Run AutoVerus on a Rust file
python autoverus.py --input src/my_module.rs --output src/my_module_verified.rs

La sortie est un fichier Rust annoté avec des clauses requires, ensures et invariant. Révisez chaque annotation. Puis exécutez Verus :

verus src/my_module_verified.rs

Si Verus rapporte verification results:: verified, le solveur SMT a dischargé toutes les obligations. S’il rapporte des erreurs, refeedez-les dans AutoVerus pour une autre ronde de réparation ou corrigez-les manuellement.

Pour l’intégration CI, traitez Verus comme un job séparé qui ne s’exécute que sur les modules annotés. Le temps de vérification de Verus croît avec la complexité des annotations. Commencez par les fonctions qui vous effraient : les parsers, les protocol state machines, tout ce qui indexe dans des buffers non fiables.

Quand utiliser AutoVerus et quand s’éloigner

AutoVerus vaut la peine d’être essayé lorsque vous avez du code Rust qui correspond au subset de Verus et que vous voulez des proofs de correction unbounded. Kani vous donne des proofs bounded sans annotations, ce qui est plus rapide pour les vérifications de crash-freedom mais ne peut pas prouver de propriétés sur des loops unbounded. AutoVerus vous donne le proof unbounded complet, au prix d’annotations qu’il génère principalement pour vous.

Éloignez-vous si votre code est async, utilise des closures complexes ou nécessite des proofs sur des propriétés de liveness comme “every request eventually gets a response”. Pour la liveness, vous voulez toujours TLA+. Éloignez-vous si votre proof nécessite une mathematical theory personnalisée. Les agents LLM n’inventent pas de nouvelles mathématiques. Ils récupèrent et adaptent des patterns qu’ils ont déjà vus.

La conclusion honnête

AutoVerus n’élimine pas la nécessité de comprendre votre code. Il élimine la nécessité de passer quarante heures à écrire des invariants pour du code que vous comprenez déjà. Le changement est de proof engineering à prompt engineering : vous décrivez l’intention, les agents search dans le proof space, et le solveur SMT certifie le résultat.

Ce changement suffit à faire passer la vérification formelle d’une niche de spécialistes à une étape de la pipeline CI. Pour les trente lignes de code de parsing entre votre application et l’entrée réseau non fiable, il est désormais pratique de prouver qu’elles ne paniqueront pas. Le proof est généré en secondes, vérifié en minutes, et révisé par un humain qui sait ce que le parser est censé faire.

Commencez par une fonction. Écrivez le Rust. Exécutez AutoVerus. Lisez les annotations. Si elles correspondent à votre intention, vous avez un proof vérifié par machine. Sinon, vous avez un point de départ meilleur qu’une page blanche.

---

Frequently Asked Questions

What is AutoVerus and how does it relate to Verus?

AutoVerus is an automated proof generation system built on top of Verus, a Rust verifier from Microsoft Research. Verus checks whether annotated Rust code satisfies its specifications using an SMT solver. AutoVerus generates those annotations using a network of LLM agents.

How accurate is AutoVerus at generating proofs?

On its benchmark of 150 non-trivial Rust proof tasks, AutoVerus achieved over 90% automation. More than half resolved in under 30 seconds or three LLM calls. Accuracy depends on how closely your code matches the training distribution patterns.

Does AutoVerus eliminate the need to learn formal verification?

No. You still need to understand the annotations to review them for correctness. A generated proof that passes verification may prove the wrong property if the LLM misread your intent. AutoVerus reduces proof writing time from days to minutes, but it does not replace human judgment.

What Rust code works with AutoVerus?

Code that fits the Verus subset: functions with loops, array indexing, arithmetic, and recursive structures. AutoVerus does not support async, closures, or many standard library collections. It is best suited for systems code, parsers, and algorithmic functions.

How much does AutoVerus cost to run?

The benchmark tasks cost cents per proof. A full module might cost ten to thirty dollars in API calls. This is significantly less than the 40 to 80 hours of engineering time required for manual proof writing.