Flux: Liquid Types for Rust
summary
Flux implements a novel refined type system for Rust as a plug-in to the Rust compiler that indexes mutable locations, introduces strong references for precise strong updates, and keeps refinements quantifier-free so liquid inference can synthesize loop and quantified container invariants automatically. Soundness relies on the Stacked Borrows aliasing model. Evaluation shows verification-spec lines cut by ~2×, verification time reduced by an order of magnitude, annotation overhead fall from up to 24% (avg 14%) to zero, and a full port of the WAVe WebAssembly sandbox is verified.
AI-written summary · about
chapters (9)
- 0:00Flux and liquid types
- 2:58Extending Rust with refinements
- 4:44Refinements and Rust ownership
- 7:57Precise updates with strong refs
- 10:03Verifying refined vectors API
- 12:50Quantitative evaluation of Flux
- 13:51Porting Wave with Flux
- 14:34Summary and availability
- 15:01Q&A
related talks
17mRefinedRust: A Type System for High-Assurance Verification of Rust Programs
01h 02mHydroflow: A Compiler Target for Fast, Correct Distributed Programs
37mCraig's Amazing Rust Spectacular
14mFluid Quotes: Metaprogramming across Abstraction Boundaries with Dependent Types
41mFunctional Rust - An Exploration
40mRust’s approach of getting things right
16mWhy Rust is the Ideal Language for Vibe-Coding
01h 05mAll the Languages Together