9 posts
AutoVerus uses a network of LLM agents to generate Verus correctness proofs for Rust code, automating over 90% of proof obligations through a...
The hardest part of formal verification has never been the verifier. It is writing the proof. Give a senior Rust engineer Verus, the SMT-based verifier from…
Large language models write surprisingly good Rust, but when you ask them for a formal proof they hallucinate invariants and invent syntax that no verifier...
LLMs can write Rust that compiles and even passes . What they cannot do reliably is write a formal proof that the code is correct for all possible inputs. The…
Model checking tools like Kani let you verify Rust properties with assertions instead of formal proofs.
You can prove Rust code correct without writing a single proof. The tool that does it is called a model checker, and for Rust the most practical one right now…
Rust's standard library grants ambient filesystem authority to every dependency.
Any crate in your dependency tree can open , write to your directory, or enumerate every file in your project. Rust's standard library does not ask for…
Thrown exceptions hide failure paths from your type system.
Your function signature says it returns a . It doesn't. It returns a or it explodes. The type system just doesn't know about the second branch. This is the…
A single-field wrapper struct catches unit-mixing bugs and type confusion without adding a single byte of overhead.
Pass a user ID to a function that expects an order ID, and Rust will not complain. Both are . The compiler sees identical types, so it cannot help you. You…
cargo-mutants finds the tests that only pretend to verify your code.
You have 100% line coverage. Every branch is hit. Every function is called. Then someone changes a to a in your pricing logic, runs the tests, and they all…
Example-based testing only covers the inputs you thought of.
You wrote a function. You tested it with and . It passes. You ship it. A user passes a single-element slice. Your function drops it on the floor. They open an…
Rust strips debug assertions automatically, but real design-by-contract needs more than debug_assert!.
Rust can enforce runtime contracts in development and erase them completely from release builds. The catch is that the language does not treat contracts as a…