Bagian tersulit dari verifikasi formal tidak pernah ada pada verifier-nya. Ada pada penulisan proof.
Beri seorang engineer Rust senior Verus, verifier berbasis SMT dari Microsoft Research, dan mereka dapat menganotasi fungsi dengan precondition dan postcondition dalam satu sore. Verifier kemudian akan memberitahu mereka, dengan kepastian mekanis, apakah fungsi tersebut memenuhi contract-contract tersebut untuk setiap input yang mungkin. Bagian itu memuaskan.
Kemudian mereka menemukan sebuah loop. Verifier mengeluh bahwa ia tidak dapat membuktikan postcondition. Engineer membutuhkan sebuah invariant, pernyataan logis yang benar sebelum dan setelah setiap iterasi. Menemukan invariant itu dulu memerlukan gelar PhD, atau setidaknya empat puluh jam trial and error. AutoVerus, dipublikasikan di OOPSLA 2025, mengotomatisasi lebih dari 90% pekerjaan itu menggunakan jaringan agent LLM. Tugas proof median terselesaikan dalam waktu kurang dari 30 detik atau tiga panggilan LLM.
Berikut cara kerjanya sebenarnya, apa biayanya, dan di mana ia masih gagal.
Bottleneck Sebenarnya adalah Pencarian Invariant, Bukan SMT Solver
Verus memperluas Rust dengan ghost code, precondition, dan postcondition. Anda menulis sesuatu seperti ini:
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
}
}Klausa requires adalah precondition. Klausa ensures adalah postcondition. Blok invariant di dalam loop while adalah apa yang membuat proof berhasil. Ia memberi tahu SMT solver apa yang tetap benar pada setiap iterasi.
Bagian sulitnya adalah invariant. total == spec_sum(arr@.subrange(0, i as int)) tidak jelas. Manusia menulisnya dengan berpikir secara induktif tentang apa yang tetap benar setelah memproses elemen-elemen pertama i. AutoVerus menghasilkan ini secara otomatis dengan memperlakukan sintesis invariant sebagai masalah search yang dipandu oleh feedback verifier.
Cara AutoVerus Menggunakan Agent LLM sebagai Strategi Search
AutoVerus bukan satu prompt ke GPT-4. Ia adalah pipeline agent-agent khusus yang saling melewatkan konteks terstruktur.
Agent pertama membaca fungsi Rust Anda dan doc comment-nya. Ia mengekstrak verification conditions dan menghasilkan draft awal klausa requires, ensures, dan invariant.
Agent kedua memasukkan anotasi-anotasi ini ke Verus. Verus mengompilasi kode yang dianotasi dan meminta SMT solver-nya, biasanya Z3, untuk mendischarge proof obligations. Jika solver mengatakan UNSAT, properti tersebut berlaku. Jika ia mengatakan SAT, ia menghasilkan sebuah counterexample. Sebagian besar waktu, draft pertama gagal.
Agent perbaikan membaca pesan error verifier dan proof obligation yang gagal. Ia menyarankan invariant yang lebih kuat, bound yang lebih ketat, atau auxiliary lemma. Siklus berulang: generate, verify, repair. AutoVerus melaporkan konvergensi median tiga panggilan LLM. Lebih dari separuh dari 150 tugas benchmark non-trivial selesai dalam waktu kurang dari 30 detik.
Wawasan yang didapat bukanlah bahwa LLM brilian dalam logika. Pencarian proof adalah masalah optimasi lokal, dan LLM cukup baik dalam menebak perbaikan lokal untuk menavigasi ruang lebih cepat daripada manusia yang mengetik dengan tangan.
Apa Arti Angka 90% Sebenarnya
AutoVerus mencapai otomatisasi proof lebih dari 90% pada benchmark 150 tugas proof Rust non-trivial. Ini mencakup array bounds reasoning, loop accumulation, dan recursive structure traversal. Benchmark diambil dari codebase Verus nyata.
Angka 90% berarti pipeline LLM menghasilkan proof yang Verus terima tanpa intervensi manusia. Ini tidak berarti specification adalah apa yang programmer maksudkan. LLM menyimpulkan intent dari nama fungsi, doc comment, dan type signature. Jika fungsi Anda bernama process dan doc comment Anda berkata “handles the thing”, specification yang dihasilkan akan bersifat generik dan mungkin salah.
Ini adalah pembagian kerja yang sama yang diperkenalkan copilot untuk code generation. LLM menulis draft pertama. Manusia meninjaunya untuk domain correctness. Perbedaannya adalah proof yang salah bersifat silent. Proof yang dihasilkan yang lolos verifikasi mungkin membuktikan properti yang salah. Anda masih membutuhkan manusia yang memahami apa yang seharusnya dilakukan fungsi tersebut.
Apa yang Tidak Dapat Dilakukan AutoVerus
AutoVerus dibatasi oleh apa yang dapat diekspresikan Verus. Verus menangani subset dari Rust. Ia tidak mendukung async, closures, atau koleksi standard library tertentu. Jika kode Anda memunculkan tasks dengan tokio, AutoVerus belum dapat membantu Anda.
AutoVerus juga terikat pada pattern. Tingkat keberhasilan 90% berlaku untuk kode yang terlihat seperti distribusi pelatihan: loop melalui array, akumulasi aritmatika, bounds checking. Jika proof Anda memerlukan auxiliary lemma yang tidak jelas, agent perbaikan mungkin berloop hingga mencapai batas iterasinya. Pada saat itu, Anda kembali menulis proof dengan tangan.
Biayanya juga tidak nol. Tugas-tugas benchmark berbiaya cents per proof. Satu module penuh mungkin berbiaya sepuluh hingga tiga puluh dolar dalam panggilan API. Itu dua orde magnitudo lebih murah dari waktu engineer verifikasi, tetapi tidak gratis.
Menjalankan AutoVerus pada Kode Nyata
AutoVerus tersedia dari Microsoft Research. Repository-nya adalah microsoft/verus-proof-synthesis di GitHub. Ia mengharuskan Anda memiliki Verus yang terinstal.
Berikut workflow praktisnya:
# 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.rsOutput-nya adalah file Rust yang dianotasi dengan klausa requires, ensures, dan invariant. Tinjau setiap anotasi. Kemudian jalankan Verus:
verus src/my_module_verified.rsJika Verus melaporkan verification results:: verified, SMT solver telah mendischarge semua obligations. Jika ia melaporkan error, umpankan kembali ke AutoVerus untuk putaran perbaikan lain atau perbaiki secara manual.
Untuk integrasi CI, perlakukan Verus sebagai job terpisah yang hanya berjalan pada module-module yang dianotasi. Waktu verifikasi Verus bertambah seiring dengan kompleksitas anotasi. Mulailah dengan fungsi yang membuat Anda takut: parser, protocol state machines, apa pun yang mengindeks ke dalam buffer yang tidak tepercaya.
Kapan Menggunakan AutoVerus dan Kapan Berhenti
AutoVerus layak dicoba ketika Anda memiliki kode Rust yang sesuai dengan subset Verus dan Anda ingin proof kebenaran yang unbounded. Kani memberikan proof bounded tanpa anotasi, yang lebih cepat untuk pemeriksaan crash-freedom tetapi tidak dapat membuktikan properti melalui loop unbounded. AutoVerus memberikan proof unbounded penuh, dengan biaya memerlukan anotasi yang sebagian besar dihasilkan untuk Anda.
Berhenti jika kode Anda async, menggunakan closures yang kompleks, atau memerlukan proof tentang properti liveness seperti “every request eventually gets a response”. Untuk liveness, Anda masih menginginkan TLA+. Berhenti jika proof Anda memerlukan mathematical theory kustom. Agent-agent LLM tidak menemukan matematika baru. Mereka mengambil dan menyesuaikan pattern yang pernah mereka lihat sebelumnya.
Garis Bawah yang Jujur
AutoVerus tidak menghilangkan kebutuhan untuk memahami kode Anda. Ia menghilangkan kebutuhan untuk menghabiskan empat puluh jam menulis invariant untuk kode yang sudah Anda pahami. Perubahannya adalah dari proof engineering ke prompt engineering: Anda menggambarkan intent, agent-agent melakukan search di proof space, dan SMT solver menyertifikasi hasilnya.
Perubahan itu cukup untuk memindahkan verifikasi formal dari niche spesialisasi ke langkah pipeline CI. Untuk tiga puluh baris kode parsing antara aplikasi Anda dan input jaringan yang tidak tepercaya, kini praktis untuk membuktikan bahwa mereka tidak akan panic. Proof dihasilkan dalam hitungan detik, diperiksa dalam hitungan menit, dan ditinjau oleh manusia yang tahu apa yang seharusnya dilakukan parser.
Mulailah dengan satu fungsi. Tulis Rust-nya. Jalankan AutoVerus. Baca anotasi-anotasinya. Jika cocok dengan intent Anda, Anda memiliki proof yang diperiksa oleh mesin. Jika tidak, Anda memiliki titik awal yang lebih baik daripada halaman kosong.
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.