AntTech
Oct 29, 2026 · Information Security
LLM-Driven Rust Formal Verification at Scale: KaPilot & KVerus
Ant Group's research institute introduces KaPilot and KVerus, two LLM-powered agent systems that automate formal verification of Rust code at scale — KaPilot verifies memory safety of Unsafe Rust via Kani model checking, while KVerus proves functional correctness using Verus deductive verification — demonstrated on the Asterinas OS kernel and Rust standard library with 29/29 verification challenges solved and 274 APIs verified.
AI-assisted verificationAsterinas OSKani
0 likes · 14 min read