Low-level pointer-manipulating programs are hard to verify, requiring complex spatial program logics that support reasoning about aliasing and separation. Worse, when working over collections, these logics burden the programmer with annotating loops with quantified invariants that describe the contents of the collection. In this talk, I will give a demo of Flux, a static verifier for Rust that shows how logical refinements can work hand in glove with Rust’s ownership mechanisms to yield ergonomic type-based verification for low-level imperative code. By factoring complex invariants into type constructors and simple refinements, Flux can efficiently synthesize loop annotations via liquid inference. We use a suite of vector-manipulating programs to demonstrate the advantages of Flux’s refinement types over program logics, as implemented in the state-of-the-art Prusti verifier.