research
VeriStruct automates formal verification of Rust data structures with 99.2% function success rate
Researchers have introduced VeriStruct, a framework that extends AI-assisted formal verification from individual functions to complete data structure modules in Verus. The system successfully verified 128 of 129 functions (99.2%) across eleven Rust data structure modules by using a planner module to generate abstractions, type invariants, and proof code, with automatic error correction for Verus syntax.