AutoVerus transforme 40 heures d'écriture de proof en 3 appels LLM. L'astuce consiste à savoir quand abandonner.
AutoVerus utilise un réseau d'agents LLM pour générer des proofs de correction Verus pour du code Rust, automatisant plus de 90% des proof obligations via une boucle générer-réparer-discharger pilotée par le feedback du solveur SMT.
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…