Automatically Enforcing Rust Trait Properties
summary
A VS Code tool automatically generates trait-check harnesses and uses Kani bounded verification to assert trait invariants (equality reflexivity/symmetry/transitivity, partial/total order, From/Into, AsMut/AsRef). It runs 42 harnesses across six crates with most checks under 10s, integrates an add trait test button and one-click run, and reports concrete counterexamples; it discovers practical bugs such as a potential multiplication overflow in PROST!'s year-to-seconds conversion and overall found 3 issues in PROST!.
AI-written summary · about
related talks
36mRust's trait system is a proof engine, let's make it prove us an ABI!
21mA Tour of Empirical Verification in Rust
19mA Hybrid Approach to Semi-automated Rust Verification
25m"Compiler-Driven Development: Making Rust Work for You"
31mValidating Rust for industry: Certification meets formal analysis
58mRust for The Curious C++ Developers
30mDebugging Trait Errors as Logic Programs
32mBuilding and Maintaining Rust at Scale