Latest News

The changing role of finite-state model checking

Foundational Verification of Running-Time Bounds for Interactive Programs

Improving system safety with Temporal Logic of Actions (TLA+)

An Anecdote Against Slop Artifacts

Domain-specific hyperspecialization (for SAT)

How to Find Bugs in Systems That Don't Exist

Why Rocq is better than Lean for program verification

A write-up on why I don't give in to the hype and switch to Lean for formal verification of programs. Comments

Fast DEFLATE compression in Lean

Xavier Leroy on programming, languages and formal verification

Extending MVCC to be serializable, in TLA+ (2024)

Introduction to Formal Verification with Lean (Part 1)

A Rust-to-Lean verification pipeline with AI provers: An experience report

Proving the Fundamental Theorem of Arithmetic in Agda

Formal methods and the future of programming

EC2’s formally verified “isolation engine” provides mathematical assurance of virtual-machine isolation

hax: A Rust verification tool

Announcing Isabelle support for SAW

A blueprint for formal verification of Apple corecrypto

Who Builds a House Without Drawing Blueprints? (2015)

How we used Quint to find over 10 bugs in SQLite while hardening Turso

Using algebra and LLMs to verify a flight-plan bug fix in Lean