The Rust type system provides strong compile-time guarantees.However, some properties cannot be fully verified by the compiler.S pecifically,p roperties likep anic freedom and memory safety in mixed safe-unsafe code requirev erification beyond what the language enforces.We exploreh ow to verify these properties in real-world Rust code using SEABMC, a bounded model checker that ingests LLVM-IR generated by the Rust compiler.W ed emonstrate our approach throught wo case studies.In the first, we develop unit proofs forf unctional properties of four data-structurelibraries: SMALLVEC, TINYVEC, SEAV EC,a nd RESULT-TYPE from the Rust standard library.These unit proofs arec heckable by both SEABMC and KANI, as tate-of-the-art bounded model checker forR ust, and we find that SeaBMC verifies these units an order of magnitude faster than Kani.The second case study focuses on verifying panic freedom of Wasmtime'sW INCH compiler.T his applicationi s drivenb yt he requirement forh igh reliability when compiling WA SM smart-contracts in the Stellarn etwork.This case study highlights that executable counterexamples from SEABMCa re highly effective forl ocalizing issues and discovering invariants.Our main contributions are( 1) an ew tool forR ust verification which, on our benchmarks, is an order of magnitude faster than KANI,( 2) twoc ase studies with reusable benchmarking and testing infrastructure, and (3) practical guidelines stemming from our experience verifying real-world code-bases.
Tafese et al. (Wed,) studied this question.