A parte mais difícil da verificação formal nunca foi o verificador. É escrever o proof.
Dê a um engenheiro sênior de Rust o Verus, o verificador baseado em SMT da Microsoft Research, e ele pode anotar uma função com preconditions e postconditions em uma tarde. O verificador então dirá a ele, com certeza mecânica, se a função satisfaz esses contracts para cada entrada possível. Essa parte é satisfatória.
Então ele encontra um loop. O verificador reclama que não pode estabelecer a postcondition. O engenheiro precisa de um invariant, uma declaração lógica que é verdadeira antes e depois de cada iteração. Encontrar esse invariant costumava exigir um PhD, ou pelo menos quarenta horas de trial and error. O AutoVerus, publicado na OOPSLA 2025, automatiza mais de 90% desse trabalho usando uma rede de agents LLM. A tarefa de proof mediana se resolve em menos de 30 segundos ou três chamadas de LLM.
Aqui está como ele realmente funciona, o que custa e onde ainda quebra.
O Gargalo Real é a Busca por Invariant, Não o Solver SMT
O Verus estende o Rust com ghost code, preconditions e postconditions. Você escreve algo assim:
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
}
}A cláusula requires é a precondition. A cláusula ensures é a postcondition. O bloco invariant dentro do loop while é o que faz o proof prosseguir. Ele diz ao solver SMT o que permanece verdadeiro em cada iteração.
A parte difícil é o invariant. total == spec_sum(arr@.subrange(0, i as int)) não é óbvio. Um humano o escreve pensando indutivamente sobre o que permanece verdadeiro após processar os primeiros i elementos. O AutoVerus gera isso automaticamente tratando a síntese de invariant como um problema de search guiado pelo feedback do verificador.
Como o AutoVerus Usa agents LLM como Estratégia de Search
O AutoVerus não é um único prompt para o GPT-4. É uma pipeline de agents especializados que passam contexto estruturado uns para os outros.
O primeiro agent lê sua função Rust e seus doc comments. Ele extrai as verification conditions e gera um rascunho inicial das cláusulas requires, ensures e invariant.
O segundo agent alimenta essas anotações no Verus. O Verus compila o código anotado e pede ao seu solver SMT, geralmente o Z3, para discharge as proof obligations. Se o solver disser UNSAT, a propriedade se mantém. Se disser SAT, ele produz um counterexample. Na maioria das vezes, o primeiro rascunho falha.
O agent de reparo lê a mensagem de erro do verificador e a proof obligation que falhou. Ele sugere um invariant mais forte, um bound mais apertado ou um auxiliary lemma. O ciclo se repete: gerar, verificar, reparar. O AutoVerus relata uma convergência mediana de três chamadas de LLM. Mais da metade das 150 tarefas de benchmark não triviais terminam em menos de 30 segundos.
A ideia não é que os LLMs sejam brilhantes em lógica. A busca por proof é um problema de otimização local, e os LLMs são bons o suficiente em adivinhar melhorias locais para navegar o espaço mais rápido do que um humano digitando manualmente.
O Que a Cifra de 90% Realmente Significa
O AutoVerus alcançou mais de 90% de automação de proof em um benchmark de 150 tarefas de proof de Rust não triviais. Elas incluíam raciocínio de array bounds, acumulação de loop e traversal de estruturas recursivas. O benchmark foi extraído de codebases reais do Verus.
A cifra de 90% significa que a pipeline de LLM gerou um proof que o Verus aceitou sem intervenção humana. Não significa que a specification é o que o programador pretendia. O LLM infere a intenção dos nomes de função, doc comments e type signatures. Se sua função se chama process e seu doc comment diz “handles the thing”, a specification gerada será genérica e possivelmente errada.
Essa é a mesma divisão de trabalho que os copilots introduziram para geração de código. O LLM escreve o primeiro rascunho. O humano o revisa para correctness de domínio. A diferença é que um proof errado é silencioso. Um proof gerado que passa na verificação pode provar a propriedade errada. Você ainda precisa de um humano que entenda o que a função deveria fazer.
O Que o AutoVerus Não Pode Fazer
O AutoVerus é limitado pelo que o Verus pode expressar. O Verus lida com um subset de Rust. Não suporta async, closures ou certas coleções da standard library. Se seu código spawna tasks com tokio, o AutoVerus ainda não pode ajudá-lo.
O AutoVerus também está ligado a patterns. A taxa de sucesso de 90% se aplica a código que se parece com a distribuição de treinamento: loops sobre arrays, acumulação aritmética, bounds checking. Se seu proof exigir um auxiliary lemma não óbvio, o agent de reparo pode fazer loop até atingir seu limite de iteração. Nesse ponto, você volta a escrever o proof manualmente.
O custo também não é zero. As tarefas de benchmark custam cents por proof. Um module completo pode custar de dez a trinta dólares em chamadas de API. Isso é duas ordens de magnitude mais barato do que o tempo de um engenheiro de verificação, mas não é gratuito.
Executando o AutoVerus em Código Real
O AutoVerus está disponível na Microsoft Research. O repository é microsoft/verus-proof-synthesis no GitHub. Ele espera que você tenha o Verus instalado.
Aqui está o workflow prático:
# 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.rsA saída é um arquivo Rust anotado com cláusulas requires, ensures e invariant. Revise cada anotação. Depois execute o Verus:
verus src/my_module_verified.rsSe o Verus reportar verification results:: verified, o solver SMT discharge todas as obligations. Se reportar erros, alimente-os de volta ao AutoVerus para outra rodada de reparo ou corrija manualmente.
Para integração com CI, trate o Verus como um job separado que roda apenas em modules anotados. O tempo de verificação do Verus cresce com a complexidade das anotações. Comece com as funções que o assustam: parsers, protocol state machines, qualquer coisa que indexe em buffers não confiáveis.
Quando Usar o AutoVerus e Quando Ir Embora
O AutoVerus vale a pena tentar quando você tem código Rust que se encaixa no subset do Verus e quer proofs de correção unbounded. O Kani dá proofs bounded sem anotações, o que é mais rápido para verificações de crash-freedom, mas não pode provar propriedades sobre loops unbounded. O AutoVerus dá o proof unbounded completo, ao custo de precisar de anotações que ele gera principalmente para você.
Vá embora se seu código for async, usar closures complexas ou exigir proofs sobre propriedades de liveness como “every request eventually gets a response”. Para liveness, você ainda quer o TLA+. Vá embora se seu proof exigir uma mathematical theory customizada. Os agents LLM não inventam nova matemática. Eles recuperam e adaptam patterns que já viram antes.
A Conclusão Honesta
O AutoVerus não elimina a necessidade de entender seu código. Ele elimina a necessidade de passar quarenta horas escrevendo invariants para código que você já entende. A mudança é de proof engineering para prompt engineering: você descreve a intenção, os agents fazem search no proof space, e o solver SMT certifica o resultado.
Essa mudança é suficiente para mover a verificação formal de um nicho de especialistas para uma etapa da pipeline de CI. Para as trinta linhas de código de parsing entre sua aplicação e a entrada de rede não confiável, agora é prático provar que elas não vão dar panic. O proof é gerado em segundos, verificado em minutos e revisado por um humano que sabe o que o parser deveria fazer.
Comece com uma função. Escreva o Rust. Execute o AutoVerus. Leia as anotações. Se elas corresponderem à sua intenção, você tem um proof verificado por máquina. Se não, você tem um ponto de partida melhor do que uma página em branco.
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.