AutoVerus mengubah 40 jam penulisan proof menjadi 3 panggilan LLM. Triknya adalah tahu kapan harus menyerah.
AutoVerus menggunakan jaringan agen LLM untuk menghasilkan proof kebenaran Verus untuk kode Rust, mengotomatisasi lebih dari 90% proof obligation melalui loop generate-repair-discharge yang didorong oleh feedback SMT solver.
Bagian tersulit dari verifikasi formal tidak pernah ada pada verifier-nya. Ada pada penulisan proof. Beri seorang engineer Rust senior Verus, verifier berbasis…