verification

5 posts

Did anyone actually verify 10,000 lines with zero defects? IBM did, and the methodology is stranger than the result.

Cleanroom software engineering promised zero-defect increments through mathematical verification instead of debugging.

The software industry average in the 1980s was 30 to 60 defects per thousand lines of code. IBM's Cleanroom team shipped a 20,000-line compiler increment with…

July 25, 2026

model-checking autoverus rust verification

AutoVerus turns 40 hours of proof writing into 3 LLM calls. The trick is knowing when to give up.

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…

July 9, 2026

model-checking temporal-logic formal-methods verification

You Can Model-Check Code Without Learning Temporal Logic

Bounded model checkers like Kani and relational model finders like Alloy let you verify properties with ordinary assertions and constraints.

You don't need to learn linear temporal logic to use a model checker. Tools like Kani, CBMC, and Alloy let you verify properties with ordinary assertions and…

July 6, 2026

model-checking rust verification formal-methods

You can prove Rust code correct without writing a single proof, but the state space is the bill

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…

July 5, 2026

n-version-programming equivalence-testing formal-methods verification

Testing Won't Prove Two Functions Are Equivalent. Here's What Will.

N-version programming assumes your implementations agree.

You built an n-version system. Three independent implementations of the same critical function, a voter that picks the majority result, and a warm feeling that…

June 14, 2026