Tag

Formal Methods

Formal methods apply mathematical logic and algebra to the specification, verification, and synthesis of software and hardware systems. The core tools include type systems (operational semantics, substructural logics, dependent types), model checking (LTL, CTL, bisimulation), theorem proving (Lean 4, Coq, Isabelle), and process algebras (CCS, CSP, the pi-calculus). In systems programming, formal methods appear as memory safety proofs (RustBelt, Iris), verified concurrent data structures (linearizability proofs), and certified compilers (CompCert). In mathematics, the Lean 4 Mathlib library provides a machine-checked foundation for undergraduate through research-level results.

Blog

June 20, 2026
Causal Models of Concurrency
From labelled transition systems and bisimulation through Mazurkiewicz traces and event structures to happens-before, logical clocks, and the observability coefficient: a mathematical account of what it means for a concurrent system to be causally intelligible.