Member-only story
🦀 Verifying Rust Code - Basic
From the borrow checker to an independent oracle
Rust programmers get a head start that most languages never offer. In safe Rust, the type system and the borrow checker already prove that your program has no use-after-free, no double free and no data race. That claim is not marketing: the RustBelt project formalised the ownership discipline in the Iris framework on top of the Rocq proof assistant and showed it sound. Every time cargo build succeeds, you have a machine-checked proof of a property that C programmers spend careers chasing with sanitizers.
It is also the point where most people stop thinking about verification, and that is a mistake. The borrow checker says nothing about whether your decoder panics on a truncated buffer, whether an addition overflows, whether the code inside an unsafe block upholds the invariants it promises, or whether the function computes the right answer at all. Those are the questions left over, and they are the ones that bite.
This two-part series walks up the ladder of techniques that answer those questions, from the cheapest to the most demanding. This first part covers everything that runs code: lints, Miri, property tests, fuzzing and differential testing against an independent oracle. The second part climbs into proofs. Both use the same real project as a running…
