Самая сложная часть формальной верификации никогда не заключалась в verifier. Она заключается в написании proof.

Дайте опытному инженеру по Rust Verus — verifier на основе SMT от Microsoft Research, — и он сможет аннотировать функцию preconditions и postconditions за один вечер. Затем verifier скажет ему с механической точностью, удовлетворяет ли функция этим contracts для каждого возможного входа. Эта часть доставляет удовлетворение.

Затем он сталкивается с loop. Verifier жалуется, что не может установить postcondition. Инженеру нужен invariant — логическое утверждение, истинное до и после каждой итерации. Раньше для поиска этого invariant требовалась степень PhD или как минимум сорок часов trial and error. AutoVerus, опубликованный на OOPSLA 2025, автоматизирует более 90% этой работы с помощью сети агентов LLM. Медианная задача proof решается менее чем за 30 секунд или за три вызова LLM.

Вот как это работает на самом деле, во что это обходится и где всё ещё ломается.

Настоящее узкое место — поиск invariant, а не SMT-solver

Verus расширяет Rust ghost-кодом, preconditions и postconditions. Вы пишете что-то вроде этого:

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
    }
}

Клауза requires — это precondition. Клауза ensures — это postcondition. Блок invariant внутри loop while — это то, что позволяет proof пройти. Он сообщает SMT-solver, что остаётся истинным на каждой итерации.

Сложная часть — это invariant. total == spec_sum(arr@.subrange(0, i as int)) неочевиден. Человек пишет его, индуктивно размышляя о том, что остаётся истинным после обработки первых i элементов. AutoVerus генерирует это автоматически, рассматривая синтез invariant как задачу search, управляемую обратной связью verifier.

AutoVerus — это не один prompt в GPT-4. Это pipeline специализированных агентов, передающих друг другу структурированный контекст.

Первый агент читает вашу функцию на Rust и её doc comments. Он извлекает verification conditions и генерирует начальный draft клауз requires, ensures и invariant.

Второй агент подаёт эти аннотации в Verus. Verus компилирует аннотированный код и просит свой SMT-solver, обычно Z3, discharge proof obligations. Если solver говорит UNSAT, свойство выполняется. Если SAT — он выдаёт counterexample. В большинстве случаев первый draft не проходит.

Repair-агент читает сообщение об ошибке verifier и failed proof obligation. Он предлагает более сильный invariant, более жёсткий bound или auxiliary lemma. Цикл повторяется: generate, verify, repair. AutoVerus сообщает о медианной сходимости в три вызова LLM. Более половины из 150 нетривиальных benchmark-задач завершаются менее чем за 30 секунд.

Идея не в том, что LLM блестяще разбираются в логике. Proof search — это задача локальной оптимизации, а LLM достаточно хороши в угадывании локальных улучшений, чтобы искать пространство быстрее, чем человек, набирающий текст вручную.

Что на самом деле означает цифра 90%

AutoVerus достиг более 90% автоматизации proof на бенчмарке из 150 нетривиальных задач proof на Rust. Они включали рассуждения о array bounds, loop accumulation и обход рекурсивных структур. Бенчмарк был взят из реальных codebases на Verus.

Цифра 90% означает, что LLM-pipeline сгенерировала proof, который Verus принял без вмешательства человека. Это не означает, что specification соответствует тому, что задумал программист. LLM выводит intent из имён функций, doc comments и type signatures. Если ваша функция называется process, а doc comment гласит “handles the thing”, сгенерированная specification будет общей и возможно ошибочной.

Это тот же разделение труда, которое copilots ввели для генерации кода. LLM пишет первый draft. Человек проверяет его на domain correctness. Разница в том, что неправильный proof молчалив. Сгенерированный proof, прошедший верификацию, может доказывать не то свойство. Вам всё ещё нужен человек, который понимает, что функция должна делать.

Что AutoVerus не может делать

AutoVerus ограничен тем, что может выразить Verus. Verus работает с subset Rust. Он не поддерживает async, closures и некоторые коллекции стандартной библиотеки. Если ваш код спавнит tasks с помощью tokio, AutoVerus пока не может вам помочь.

AutoVerus также связан с patterns. 90% успеха относятся к коду, похожему на обучающее распределение: loops по массивам, арифметическое accumulation, bounds checking. Если ваш proof требует нетривиального auxiliary lemma, repair-агент может зациклиться до достижения лимита итераций. В этот момент вы возвращаетесь к ручному написанию proof.

Стоимость тоже не нулевая. Benchmark-задачи стоят cents за proof. Полный модуль может обойтись в десять-тридцать долларов в API-вызовах. Это на два порядка дешевле времени инженера-верификатора, но не бесплатно.

Запуск AutoVerus на реальном коде

AutoVerus доступен от Microsoft Research. Репозиторий — microsoft/verus-proof-synthesis на GitHub. Предполагается, что Verus установлен.

Вот практический 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.rs

Выход — аннотированный файл на Rust с клаузами requires, ensures и invariant. Проверьте каждую аннотацию. Затем запустите Verus:

verus src/my_module_verified.rs

Если Verus сообщает verification results:: verified, SMT-solver discharge все obligations. Если сообщает об ошибках, передайте их обратно в AutoVerus для ещё одного раунда repair или исправьте вручную.

Для интеграции с CI рассматривайте Verus как отдельный job, запускаемый только на аннотированных модулях. Время верификации Verus растёт с сложностью аннотаций. Начинайте с функций, которые вас пугают: parsers, protocol state machines, всё, что индексирует в untrusted buffers.

Когда использовать AutoVerus, а когда уходить

AutoVerus стоит попробовать, когда у вас есть код на Rust, который подходит под subset Verus, и вы хотите unbounded proofs корректности. Kani даёт bounded proofs без аннотаций, что быстрее для проверок crash-freedom, но не может доказать свойства для unbounded loops. AutoVerus даёт полный unbounded proof, за счёт необходимости в аннотациях, которые он в основном генерирует за вас.

Уходите, если ваш код async, использует сложные closures или требует proofs о свойствах liveness вроде “every request eventually gets a response”. Для liveness вам всё ещё нужен TLA+. Уходите, если ваш proof требует custom mathematical theory. Агенты LLM не изобретают новую математику. Они извлекают и адаптируют patterns, которые видели раньше.

Честный итог

AutoVerus не устраняет необходимость понимать свой код. Он устраняет необходимость тратить сорок часов на написание invariant для кода, который вы уже понимаете. Сдвиг происходит от proof engineering к prompt engineering: вы описываете intent, агенты ищут в proof space, а SMT-solver сертифицирует результат.

Этого сдвига достаточно, чтобы перенести формальную верификацию из специализированной ниши в шаг CI pipeline. Для тридцати строк parsing-кода между вашим приложением и untrusted сетевым входом теперь практично доказать, что они не вызовут panic. Proof генерируется за секунды, проверяется за минуты и рецензируется человеком, который знает, что parser должен делать.

Начните с одной функции. Напишите Rust. Запустите AutoVerus. Прочитайте аннотации. Если они соответствуют вашему intent, у вас есть machine-checked proof. Если нет — у вас есть отправная точка лучше, чем чистый лист.

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.