Practical, High-Performance Verification in Rust

AutoVerus 

2024年9月

Automatically synthesize proof annotations that help Verus prove the correctness of Rust code.