Der schwierigste Teil der formalen Verifikation war nie der Verifier. Es ist das Schreiben des Proofs.
Gib einem erfahrenen Rust-Engineer Verus, den SMT-basierten Verifier von Microsoft Research, und er kann eine Funktion in einem Nachmittag mit Preconditions und Postconditions annotieren. Der Verifier wird ihm dann mit mechanischer Sicherheit sagen, ob die Funktion diese Contracts für jede mögliche Eingabe erfüllt. Das ist befriedigend.
Dann trifft er auf eine Loop. Der Verifier beschwert sich, dass er die Postcondition nicht herleiten kann. Der Engineer braucht ein Invariant, eine logische Aussage, die vor und nach jeder Iteration wahr ist. Das Finden dieses Invariants erforderte früher einen PhD oder mindestens vierzig Stunden Trial and Error. AutoVerus, veröffentlicht auf der OOPSLA 2025, automatisiert mehr als 90% dieser Arbeit mit einem Netzwerk von LLM-Agents. Die mediane Proof-Aufgabe löst sich in unter 30 Sekunden oder drei LLM-Calls.
Hier ist, wie es wirklich funktioniert, was es dich kostet und wo es noch bricht.
Der echte Bottleneck ist die Invariant-Suche, nicht der SMT-Solver
Verus erweitert Rust um Ghost Code, Preconditions und Postconditions. Du schreibst so etwas:
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
}
}Die requires-Klausel ist die Precondition. Die ensures-Klausel ist die Postcondition. Der invariant-Block innerhalb der while-Loop ist das, was den Proof durchführt. Er sagt dem SMT-Solver, was bei jeder Iteration wahr bleibt.
Der schwierige Teil ist das Invariant. total == spec_sum(arr@.subrange(0, i as int)) ist nicht offensichtlich. Ein Mensch schreibt es, indem er induktiv darüber nachdenkt, was nach der Verarbeitung der ersten i Elemente wahr bleibt. AutoVerus generiert dies automatisch, indem es die Invariant-Synthese als Search-Problem behandelt, das vom Verifier-Feedback geleitet wird.
Wie AutoVerus LLM-Agents als Search-Strategie einsetzt
AutoVerus ist kein einzelner Prompt an GPT-4. Es ist eine Pipeline spezialisierter Agents, die strukturierten Kontext aneinander weitergeben.
Der erste Agent liest deine Rust-Funktion und ihre Doc Comments. Er extrahiert die Verification Conditions und generiert einen initialen Draft der requires, ensures und invariant-Klauseln.
Der zweite Agent füttert diese Annotationen in Verus. Verus kompiliert den annotierten Code und bittet seinen SMT-Solver, meist Z3, die Proof-Obligations zu dischargen. Wenn der Solver UNSAT sagt, gilt die Eigenschaft. Wenn er SAT sagt, produziert er ein Counterexample. Meistens schlägt der erste Draft fehl.
Der Repair-Agent liest die Verifier-Error-Message und die fehlgeschlagene Proof-Obligation. Er schlägt ein stärkeres Invariant, eine engere Bound oder ein Auxiliary-Lemma vor. Der Zyklus wiederholt sich: generieren, verifizieren, reparieren. AutoVerus meldet eine mediane Konvergenz von drei LLM-Calls. Mehr als die Hälfte der 150 nicht-trivialen Benchmark-Aufgaben schließt in unter 30 Sekunden ab.
Die Erkenntnis ist nicht, dass LLMs brillant in Logik sind. Proof-Search ist ein lokales Optimierungsproblem, und LLMs sind gut genug darin, lokale Verbesserungen zu raten, um den Raum schneller zu durchsuchen als ein Mensch, der von Hand tippt.
Was die 90%-Zahl wirklich bedeutet
AutoVerus erreichte über 90% Proof-Automation auf einem Benchmark von 150 nicht-trivialen Rust-Proof-Aufgaben. Diese umfassten Array-Bounds-Reasoning, Loop-Accumulation und rekursive Structure-Traversal. Der Benchmark stammte aus realen Verus-Codebases.
Die 90%-Zahl bedeutet, dass die LLM-Pipeline einen Proof generierte, den Verus ohne menschliches Zutun akzeptierte. Sie bedeutet nicht, dass die Specification das ist, was der Programmierer beabsichtigte. Das LLM inferiert Intent aus Funktionsnamen, Doc Comments und Type-Signatures. Wenn deine Funktion process heißt und dein Doc Comment „handles the thing“ sagt, wird die generierte Specification generisch und möglicherweise falsch sein.
Das ist dieselbe Arbeitsteilung, die Copilots für die Code-Generation eingeführt haben. Das LLM schreibt den ersten Draft. Der Mensch reviewt ihn auf Domain-Correctness. Der Unterschied ist, dass ein falscher Proof still ist. Ein generierter Proof, der die Verifikation besteht, kann die falsche Eigenschaft beweisen. Du brauchst immer noch einen Menschen, der versteht, was die Funktion tun soll.
Was AutoVerus nicht kann
AutoVerus ist durch das begrenzt, was Verus ausdrücken kann. Verus behandelt eine Subset von Rust. Es unterstützt kein async, keine Closures und bestimmte Standard-Library-Collections. Wenn dein Code Tasks mit tokio spawnt, kann AutoVerus dir noch nicht helfen.
AutoVerus ist auch Pattern-gebunden. Die 90%-Erfolgsrate gilt für Code, der wie die Training-Distribution aussieht: Loops über Arrays, arithmetische Accumulation, Bounds-Checking. Wenn dein Proof ein nicht-offensichtliches Auxiliary-Lemma erfordert, kann der Repair-Agent loopen, bis er sein Iterationslimit erreicht. Dann bist du wieder dabei, den Proof von Hand zu schreiben.
Die Kosten sind auch nicht null. Die Benchmark-Aufgaben kosten Cents pro Proof. Ein vollständiges Modul kann zehn bis dreißig Dollar in API-Calls kosten. Das ist zwei Größenordnungen billiger als die Zeit eines Verification-Engineers, aber es ist nicht kostenlos.
AutoVerus auf echtem Code ausführen
AutoVerus ist von Microsoft Research verfügbar. Das Repository ist microsoft/verus-proof-synthesis auf GitHub. Es erwartet, dass Verus installiert ist.
Hier ist der praktische Workflow:
# 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.rsDie Ausgabe ist eine annotierte Rust-Datei mit requires, ensures und invariant-Klauseln. Review jede Annotation. Dann führe Verus aus:
verus src/my_module_verified.rsWenn Verus verification results:: verified meldet, hat der SMT-Solver alle Obligations discharged. Wenn er Fehler meldet, füttere sie zurück in AutoVerus für eine weitere Repair-Runde oder behebe sie manuell.
Für die CI-Integration behandle Verus als separaten Job, der nur auf annotierten Modulen läuft. Die Verus-Verifikationszeit wächst mit der Annotation-Komplexität. Beginne mit den Funktionen, die dir Angst machen: Parser, Protocol-State-Machines, alles, das in untrusted Buffer indiziert.
Wann AutoVerus zu nutzen ist und wann man abbricht
AutoVerus lohnt sich, wenn du Rust-Code hast, der in das Verus-Subset passt, und du unbounded Proofs of Correctness willst. Kani gibt dir bounded Proofs ohne Annotationen, was für Crash-Freedom-Checks schneller ist, aber keine Eigenschaften über unbounded Loops beweisen kann. AutoVerus gibt dir den vollständigen unbounded Proof, auf Kosten von Annotationen, die es größtenteils für dich generiert.
Brich ab, wenn dein Code async ist, komplexe Closures nutzt oder Proofs über Liveness-Eigenschaften wie „every request eventually gets a response“ erfordert. Für Liveness willst du immer noch TLA+. Brich ab, wenn dein Proof eine custom Mathematical Theory erfordert. Die LLM-Agents erfinden keine neue Mathematik. Sie retrieve und adaptieren Patterns, die sie schon gesehen haben.
Die ehrliche Bottom Line
AutoVerus eliminiert nicht die Notwendigkeit, deinen Code zu verstehen. Es eliminiert die Notwendigkeit, vierzig Stunden damit zu verbringen, Invariants für Code zu schreiben, den du bereits verstehst. Der Shift geht von Proof Engineering zu Prompt Engineering: du beschreibst den Intent, die Agents durchsuchen den Proof-Space, und der SMT-Solver zertifiziert das Ergebnis.
Dieser Shift reicht aus, um formale Verifikation von einer Spezialisten-Nische zu einem CI-Pipeline-Schritt zu machen. Für die dreißig Zeilen Parsing-Code zwischen deiner Anwendung und ungetrusted Network-Input ist es jetzt praktikabel zu beweisen, dass sie nicht paniken. Der Proof wird in Sekunden generiert, in Minuten geprüft und von einem Menschen reviewt, der weiß, was der Parser tun soll.
Beginne mit einer Funktion. Schreibe den Rust. Führe AutoVerus aus. Lies die Annotationen. Wenn sie deinem Intent entsprechen, hast du einen machine-checked Proof. Wenn nicht, hast du einen besseren Startpunkt als eine leere Seite.
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.