형식 검증에서 가장 어려운 부분은 검증기 자체가 아니다. 증명을 작성하는 것이다.

숙련된 Rust 엔지니어에게 Microsoft Research의 SMT 기반 검증기인 Verus를 주면, 오후 한때에 함수에 precondition과 postcondition을 주석으로 달 수 있다. 그러면 검증기는 기계적 확실성으로, 해당 함수가 모든 가능한 입력에 대해 그 계약을 만족하는지 알려준다. 그 부분은 만족스럽다.

그런 다음 루프를 만난다. 검증기는 postcondition을 확립할 수 없다고 불평한다. 엔지니어는 invariant, 즉 각 반복 전후에 참인 논리적 진술이 필요하다. 이 invariant를 찾는 것은 예전에는 박사 학위가 필요했거나, 최소한 사십 시간의 시행착오가 필요했다. OOPSLA 2025에 발표된 AutoVerus는 LLM 에이전트 네트워크를 사용해 이 작업의 90% 이상을 자동화한다. 중간값 기준 증명 작업은 30초 이내 또는 세 번의 LLM 호출로 해결된다.

다음은 실제 작동 방식, 비용, 그리고 여전히 한계가 있는 부분이다.

진정한 병목은 SMT 솔버가 아니라 invariant 탐색이다

Verus는 Rust를 ghost code, precondition, postcondition으로 확장한다. 다음과 같이 작성한다:

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이다. while 루프 내부의 invariant 블록은 증명이 통과하게 만드는 핵심이다. 이것은 SMT 솔버에게 각 반복에서 무엇이 참으로 남는지 알려준다.

어려운 부분은 invariant이다. total == spec_sum(arr@.subrange(0, i as int))는 자명하지 않다. 사람은 처음 i개 요소를 처리한 후 무엇이 참으로 남는지 귀납적으로 생각하며 이를 작성한다. AutoVerus는 검증기 피드백에 의해 안내되는 탐색 문제로 invariant 합성을 다룸으로써 이를 자동으로 생성한다.

AutoVerus가 LLM 에이전트를 탐색 전략으로 사용하는 방법

AutoVerus는 GPT-4에 대한 단일 프롬프트가 아니다. 구조화된 맥락을 서로 전달하는 전문화된 에이전트의 파이프라인이다.

첫 번째 에이전트는 Rust 함수와 해당 doc comment를 읽는다. verification condition을 추출하고 requires, ensures, invariant 절의 초안을 생성한다.

두 번째 에이전트는 이 주석들을 Verus에 입력한다. Verus는 주석이 달린 코드를 컴파일하고, SMT 솔버(보통 Z3)에게 proof obligation의 discharge를 요청한다. 솔버가 UNSAT라고 하면 성질이 성립한다. SAT라고 하면 counterexample을 생성한다. 대부분의 경우 첫 번째 초안은 실패한다.

수정 에이전트는 검증기 오류 메시지와 실패한 proof obligation을 읽는다. 더 강한 invariant, 더 엄격한 bound, 또는 auxiliary lemma를 제안한다. 사이클은 반복된다: 생성, 검증, 수정. AutoVerus는 중간값 기준 세 번의 LLM 호출로 수렴한다고 보고한다. 150개의 비자명한 벤치마크 작업의 절반 이상이 30초 이내에 완료된다.

통찰은 LLM이 논리에 뛰어나다는 것이 아니다. 증명 탐색은 국소 최적화 문제이며, LLM은 손으로 입력하는 사람보다 공간을 더 빠르게 탐색하기 위해 국소적 개선을 추측하는 데 충분히 능숙하다.

90%라는 숫자가 실제로 의미하는 것

AutoVerus는 150개의 비자명한 Rust 증명 작업 벤치마크에서 90% 이상의 증명 자동화를 달성했다. 여기에는 배열 경계 추론, 루프 누적, 재귀적 구조 순회가 포함되었다. 벤치마크는 실제 Verus 코드베이스에서 추출되었다.

90%라는 숫자는 LLM 파이프라인이 사람의 개입 없이 Verus가 수락한 증명을 생성했다는 의미이다. 이것이 사양이 프로그래머가 의도한 것이라는 뜻은 아니다. LLM은 함수 이름, doc comment, 타입 서명에서 의도를 추론한다. 함수가 process라고 이름 지어지고 doc comment가 “handles the thing”이라고 하면, 생성된 사양은 일반적이고 잘못되었을 가능성이 있다.

이것은 코드 생성을 위해 copilot이 도입한 것과 동일한 분업이다. LLM이 초안을 쓰고, 사람이 도메인 정확성을 위해 검토한다. 차이점은 잘못된 증명은 조용하다는 것이다. 검증을 통과한 생성된 증명은 잘못된 성질을 증명할 수 있다. 함수가 무엇을 해야 하는지 이해하는 사람은 여전히 필요하다.

AutoVerus가 할 수 없는 것

AutoVerus는 Verus가 표현할 수 있는 범위로 제한된다. Verus는 Rust의 부분 집합을 다룬다. async, closures, 특정 표준 라이브러리 컬렉션을 지원하지 않는다. 코드가 tokio로 태스크를 spawn하면 AutoVerus는 아직 도움을 줄 수 없다.

AutoVerus는 패턴에도 묶여 있다. 90%의 성공률은 훈련 분포처럼 보이는 코드, 즉 배열에 대한 루프, 산술 누적, 경계 검사에 적용된다. 증명에 자명하지 않은 auxiliary lemma가 필요하다면, 수정 에이전트는 반복 한도에 도달할 때까지 루프할 수 있다. 그 시점에서는 다시 손으로 증명을 작성하게 된다.

비용도 제로는 아니다. 벤치마크 작업은 증명당 몇 센트가 든다. 전체 모듈은 API 호출로 십에서 삼십 달러가 들 수 있다. 이는 검증 엔지니어의 시간보다 두 자릿수 저렴하지만 무료는 아니다.

실제 코드에서 AutoVerus 실행하기

AutoVerus는 Microsoft Research에서 제공한다. 저장소는 GitHub의 microsoft/verus-proof-synthesis이다. Verus가 설치되어 있을 것을 전제로 한다.

실제 워크플로우는 다음과 같다:

# 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

출력은 requires, ensures, invariant 절을 포함한 주석이 달린 Rust 파일이다. 모든 주석을 검토하라. 그런 다음 Verus를 실행한다:

verus src/my_module_verified.rs

Verus가 verification results:: verified를 보고하면 SMT 솔버가 모든 의무를 discharge한 것이다. 오류를 보고하면 AutoVerus에 다시 입력하여 또 다른 수정 라운드를 수행하거나 수동으로 수정한다.

CI 통합에서는 Verus를 주석이 달린 모듈에서만 실행되는 별도 작업으로 취급한다. Verus 검증 시간은 주석 복잡도에 따라 증가한다. 두려운 함수부터 시작하라: 파서, 프로토콜 state machine, 신뢰할 수 없는 버퍼에 인덱싱하는 모든 것.

AutoVerus를 사용해야 할 때와 포기해야 할 때

AutoVerus는 Verus 부분 집합에 맞는 Rust 코드가 있고 무한 정합성 증명을 원할 때 시도할 가치가 있다. Kani는 주석 없이 유한 증명을 제공하여 충돌 없음 검사에 더 빠르지만, 무한 루프에 대한 성질은 증명할 수 없다. AutoVerus는 완전한 무한 증명을 제공한다. 대신 대부분 자동 생성되는 주석이 필요하다.

코드가 async이거나, 복잡한 closures를 사용하거나, “모든 요청은 결국 응답을 받는다”와 같은 liveness 성질에 대한 증명이 필요한 경우 포기하라. liveness에는 여전히 TLA+가 필요하다. 사용자 정의 수학 이론이 증명에 필요한 경우에도 포기하라. LLM 에이전트는 새로운 수학을 발명하지 않는다. 이전에 본 패턴을 검색하고 적응할 뿐이다.

솔직한 결론

AutoVerus는 코드를 이해할 필요성을 없애지 않는다. 이미 이해하고 있는 코드에 대해 invariant를 사십 시간 동안 작성할 필요성을 없앤다. 변화는 proof engineering에서 prompt engineering으로의 전환이다: 의도를 서술하고, 에이전트가 증명 공간을 탐색하고, SMT 솔버가 결과를 인증한다.

이 전환은 형식 검증을 전문가의 틈새에서 CI 파이프라인 단계로 옮기기에 충분하다. 애플리케이션과 신뢰할 수 없는 네트워크 입력 사이의 삼십 줄 분석 코드에 대해, 이제 패닉하지 않음을 증명하는 것이 실용적이다. 증명은 수 초 내에 생성되고, 수 분 내에 검증되며, 파서가 무엇을 해야 하는지 아는 사람에 의해 검토된다.

한 함수부터 시작하라. Rust를 작성하라. AutoVerus를 실행하라. 주석을 읽어라. 의도와 일치하면 기계 검증된 증명을 얻은 것이다. 일치하지 않으면 백지보다 나은 출발점을 얻은 것이다.

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.