La parte más difícil de la verificación formal nunca ha sido el verificador. Es escribir el proof.
Dale a un ingeniero senior de Rust Verus, el verificador basado en SMT de Microsoft Research, y puede anotar una función con preconditions y postconditions en una tarde. El verificador le dirá entonces, con certeza mecánica, si la función satisface esos contracts para cada entrada posible. Esa parte es satisfactoria.
Luego encuentra un loop. El verificador se queja de que no puede establecer la postcondition. El ingeniero necesita un invariant, una declaración lógica que es verdadera antes y después de cada iteración. Encontrar ese invariant solía requerir un doctorado, o al menos cuarenta horas de trial and error. AutoVerus, publicado en OOPSLA 2025, automatiza más del 90% de ese trabajo utilizando una red de agents LLM. La tarea de proof mediana se resuelve en menos de 30 segundos o tres llamadas a LLM.
Aquí está cómo funciona realmente, lo que te cuesta y dónde todavía falla.
El cuello de botella real es la búsqueda de invariant, no el solver SMT
Verus extiende Rust con ghost code, preconditions y postconditions. Escribes algo como esto:
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 cláusula requires es la precondition. La cláusula ensures es la postcondition. El bloque invariant dentro del loop while es lo que hace que el proof avance. Le dice al solver SMT qué se mantiene verdadero en cada iteración.
La parte difícil es el invariant. total == spec_sum(arr@.subrange(0, i as int)) no es obvio. Un humano lo escribe pensando inductivamente sobre qué se mantiene verdadero después de procesar los primeros i elementos. AutoVerus genera esto automáticamente tratando la síntesis de invariant como un problema de búsqueda guiado por el feedback del verificador.
Cómo usa AutoVerus agents LLM como estrategia de búsqueda
AutoVerus no es un solo prompt a GPT-4. Es una pipeline de agents especializados que pasan contexto estructurado entre sí.
El primer agent lee tu función Rust y sus doc comments. Extrae las verification conditions y genera un draft inicial de las cláusulas requires, ensures e invariant.
El segundo agent alimenta estas anotaciones a Verus. Verus compila el código anotado y le pide a su solver SMT, usualmente Z3, que dischargue las proof obligations. Si el solver dice UNSAT, la propiedad se mantiene. Si dice SAT, produce un counterexample. La mayoría de las veces, el primer draft falla.
El agent de reparación lee el mensaje de error del verificador y la proof obligation fallida. Sugiere un invariant más fuerte, un bound más estricto o un auxiliary lemma. El ciclo se repite: generar, verificar, reparar. AutoVerus reporta una convergencia mediana de tres llamadas a LLM. Más de la mitad de las 150 tareas de benchmark no triviales terminan en menos de 30 segundos.
La idea no es que los LLMs sean brillantes en lógica. La búsqueda de proof es un problema de optimización local, y los LLMs son lo suficientemente buenos adivinando mejoras locales para navegar el espacio más rápido que un humano escribiendo a mano.
Lo que realmente significa la cifra del 90%
AutoVerus logró más del 90% de automatización de proof en un benchmark de 150 tareas de proof de Rust no triviales. Estas incluían razonamiento de array bounds, acumulación de loops y traversals de estructuras recursivas. El benchmark se extrajo de codebases reales de Verus.
La cifra del 90% significa que la pipeline de LLM generó un proof que Verus aceptó sin intervención humana. No significa que la specification sea lo que el programador pretendía. El LLM infiere la intención de los nombres de función, doc comments y type signatures. Si tu función se llama process y tu doc comment dice “handles the thing”, la specification generada será genérica y posiblemente incorrecta.
Esta es la misma división del trabajo que los copilots introdujeron para la generación de código. El LLM escribe el primer draft. El humano lo revisa para verificar la correctness del dominio. La diferencia es que un proof incorrecto es silencioso. Un proof generado que pasa la verificación puede probar la propiedad incorrecta. Todavía necesitas un humano que entienda lo que la función se supone que debe hacer.
Lo que AutoVerus no puede hacer
AutoVerus está limitado por lo que Verus puede expresar. Verus maneja un subset de Rust. No soporta async, closures o ciertas colecciones de la standard library. Si tu código spawnea tasks con tokio, AutoVerus aún no puede ayudarte.
AutoVerus también está ligado a patterns. La tasa de éxito del 90% se aplica a código que se parece a la distribución de entrenamiento: loops sobre arrays, acumulación aritmética, bounds checking. Si tu proof requiere un auxiliary lemma no obvio, el agent de reparación puede hacer loop hasta alcanzar su límite de iteración. En ese punto, vuelves a escribir el proof a mano.
El costo tampoco es cero. Las tareas de benchmark cuestan cents por proof. Un module completo puede costar de diez a treinta dólares en llamadas a API. Eso es dos órdenes de magnitud más barato que el tiempo de un ingeniero de verificación, pero no es gratis.
Ejecutando AutoVerus en código real
AutoVerus está disponible desde Microsoft Research. El repository es microsoft/verus-proof-synthesis en GitHub. Espera que tengas Verus instalado.
Aquí está el workflow práctico:
# 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.rsLa salida es un archivo Rust anotado con cláusulas requires, ensures e invariant. Revisa cada anotación. Luego ejecuta Verus:
verus src/my_module_verified.rsSi Verus reporta verification results:: verified, el solver SMT ha dischargue todas las obligations. Si reporta errores, aliméntalos de vuelta a AutoVerus para otra ronda de reparación o arréglalos manualmente.
Para la integración con CI, trata a Verus como un job separado que se ejecuta solo en modules anotados. El tiempo de verificación de Verus crece con la complejidad de las anotaciones. Empieza con las funciones que te asustan: parsers, protocol state machines, cualquier cosa que indexe en buffers no confiables.
Cuándo usar AutoVerus y cuándo alejarse
AutoVerus vale la pena intentarlo cuando tienes código Rust que encaja en el subset de Verus y quieres proofs de corrección unbounded. Kani te da proofs bounded sin anotaciones, lo cual es más rápido para verificaciones de crash-freedom pero no puede probar propiedades sobre loops unbounded. AutoVerus te da el proof unbounded completo, a costa de necesitar anotaciones que en su mayoría genera para ti.
Aléjate si tu código es async, usa closures complejas o requiere proofs sobre propiedades de liveness como “every request eventually gets a response”. Para liveness, todavía quieres TLA+. Aléjate si tu proof requiere una mathematical theory custom. Los agents LLM no inventan nueva matemática. Recuperan y adaptan patterns que han visto antes.
La conclusión honesta
AutoVerus no elimina la necesidad de entender tu código. Elimina la necesidad de pasar cuarenta horas escribiendo invariants para código que ya entiendes. El cambio es de proof engineering a prompt engineering: describes la intención, los agents buscan en el proof space, y el solver SMT certifica el resultado.
Ese cambio es suficiente para mover la verificación formal de un nicho de especialistas a un paso de la pipeline de CI. Para las treinta líneas de código de parsing entre tu aplicación y la entrada de red no confiable, ahora es práctico probar que no harán panic. El proof se genera en segundos, se verifica en minutos y es revisado por un humano que sabe lo que el parser se supone que debe hacer.
Empieza con una función. Escribe el Rust. Ejecuta AutoVerus. Lee las anotaciones. Si coinciden con tu intención, tienes un proof verificado por máquina. Si no, tienes un punto de partida mejor que una página en blanco.
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.