Writing
- Formal verification in practice: what to prove and how far to goA ladder from stronger types to full proofs, with what each rung catches, what it costs and how well AI agents handle it: how to choose what to prove, write specs, prove a model or the code, keep proofs working in CI, and use agents without trusting them for the spec. Every rule is graded by its evidence.Article
- Formal verification in Rust: Verus vs Kani vs Creusot (2026)How to prove Rust code correct in 2026: Verus, Kani, Creusot, Prusti, Aeneas, Flux, hax and VeriFast compared on what they prove, what Rust they handle and how well AI agents write the proofs, with one binary search through Verus and Kani. Short answer: Kani first for unsafe code and panics, Verus for full proofs.Article
