A Hybrid Approach to Semi-automated Rust Verification
summary
A prototype hybrid verifier links Gillian-Rust (symbolic-execution + separation logic) with Creusot so safe Rust specs are checked automatically while unsafe implementations get targeted, semi-automated proofs; it verifies real-world standard-library functions (about 2% unsafe code) with minor annotations, proves vec push end-to-end in under 3 seconds, and reports verification times orders of magnitude faster than comparable tools.
AI-written summary · about
chapters (9)
- 0:00Welcome
- 1:47Hybrid verification goals
- 3:33Why Rust verification now
- 6:20Unsafe code in Rust
- 8:27Hybrid verification tools
- 11:59Automations for unsafe verification
- 15:29Limitations and prototype
- 16:32Key takeaways
- 17:15Q&A
related talks
17mRefinedRust: A Type System for High-Assurance Verification of Rust Programs
21mA Tour of Empirical Verification in Rust
18mVerus: Verifying Rust Programs using Linear Ghost Types
56mRust for Safe and Scalable Automotive: Insights from
10mVerifying the Rust Standard Library
15mConveros: Practical Model Checking for Verifying Rust OS Kernel Concurrency
31mValidating Rust for industry: Certification meets formal analysis
33mVerifying the Rust Standard Library