Tag
formal-verification
- Sep 30, 2026 Litmus Tests as Executable Specifications How a five-line concurrency test becomes a machine-checkable claim, what the litmus file format encodes, and how a model checker decides which outcomes are forbidden. memory systems
- Aug 27, 2026 What a Sandbox Proof Establishes and What It Assumes How verification of a sandbox reduces the isolation guarantee to a set of machine-checked lemmas, where the specification gap appears, and why the assumptions are the part that matters. language runtimes
- Jun 3, 2026 Equivalence Checking: Proving a Netlist Matches Its RTL How combinational equivalence is reduced to a miter of two circuits and a satisfiability question, why sequential transformations break that reduction, and where the proof stops being cheap. hardware engineering
- Apr 1, 2026 Symbolic Protocol Verification and the Perfect Encryption Assumption How Dolev-Yao models reduce cryptography to term algebra, what tools such as ProVerif and Tamarin can and cannot find, and why a symbolic attack is always worth taking seriously. cryptography
- Apr 10, 2025 The Linux Kernel Memory Model and Its Tooling How LKMM formalises READ_ONCE, smp_mb, and RCU into an executable model, what its relation set adds to the architecture models, and where it deliberately diverges from C11. memory systems