Lessons Learned from Incorporating FM in Huawei Cloud Reliability
Cauli et al. (2026)
Reading Library
The CARS reading library collects essays, blog posts, and vision papers on formal methods, solver-aided programming, and software correctness. Some argue for verification, some against, some just show what happened when people tried it. Browse by title or follow whatever catches your eye. New readings may be added as the quarter progresses.
For the academic research papers cited in lectures, see the Bibliography.
Some readings may be behind publisher paywalls. As a UW student, you have free access through the UW Libraries proxy. See the Resources page for setup instructions.
The Final Bottleneck
Ronacher (2026)
Coding After Coders
Thompson (2026)
Some Silly Z3 Scripts I Wrote
Wayne (2026)
SAT/SMT by Example (book)
Yurichev (2026)
Lessons from Formally Verified Deployed Software Systems
Huang et al. (2026)
TLA+ as a Design Accelerator: Lessons from the Industry
Demirbas (2026)
When AI Writes the World's Software, Who Verifies It?
de Moura (2026)
Who Watches the Provers?
de Moura (2026)
Formal Verification in the Age of AI
Murray (2026)
LLMs versus the Halting Problem
Sultan et al. (2026)
AI Coding's Hidden Verification Premium
Thomas (2026)
Intent Formalization Grand Challenge
Lahiri et al. (2026)
LLMs and Formal Methods
Unalarming (2026)
Integrating Formal Methods and Automated Tools for DO-178C Compliance in UAV Software
Zrelli et al. (2026)
The Pragmatic Magic of Semi-Formal Methods
Antithesis (2025)
Systems Correctness Practices at AWS
Brooker, Desai (2025)
It's the Specification, Stupid!
Broy, Ruess, Shankar (2025)
The Coming Need for Formal Specification
Congdon (2025)
What Works (and Doesn't) Selling Formal Methods
Dodds (Galois) (2025)
AI Will Make Formal Verification Go Mainstream
Kleppmann (2025)
On the Impact of Formal Verification on Software Development
Mugnier et al. (2025)
Verina: Benchmarking Verifiable Code Generation
Ye et al. (2025)
How Intel Avoids the FDIV Bug
chiplog (2025)
A Conjecture Regarding SMT Instability
Cebeci et al. (2025)
Are We Serious About Using TLA+ For Statistical Properties?
Davis (2025)
Specifications Don't Exist
Dodds (Galois) (2025)
A Supposedly Worthwhile Contract I'll Never Do Again
Helwer (2025)
Minimize Generative AI Hallucinations with Amazon Bedrock Automated Reasoning
Akinfaderin (2025)
Formal or Not Formal: That Is the Question in AI for Theorem Proving
Buzzard (2025)
Vibe Coding Needs Vibe Reasoning
Mitchell (2025)
Can Large Language Models Verify System Software?
Qin et al. (2025)
The Proof Must Go On
Averill et al. (2025)
It Takes a Village: Bridging Gaps between Current and Formal Specs for Protocols
Basin et al. (2025)
Toward Practical Deductive Verification: Insights from a Qualitative Survey
Brugger et al. (2025)
Formal Methods: Just Good Engineering Practice?
Brooker (2024)
Formal Modeling and Simulation for Reliable Distributed Systems
Datadog (2024)
Why Fuzzing over Formal Verification?
Feist et al. (2024)
Mariposa: Butterfly Effect in SMT (blog)
Zhou (2024)
Satisfiability Modulo Theories: A Beginner's Tutorial
Barrett et al. (2024)
Practical Introduction to Constraint Programming Using CP-SAT
Olivier (2024)
Crux: A Precise Verifier for Rust and Other Languages
Pernsteiner et al. (2024)
Compiling With Constraints
Zucker (2024)
Obtaining Statistical Properties Through Modeling and Simulation
Vanlightly (2024)
Verifying Kafka Transactions: Diary Entry 3
Vanlightly (2024)
Applying Continuous Formal Methods to Cardano
Chapman et al. (2024)
Thoughts on The Future of TLA+
Wayne (2024)
Mariposa: Measuring SMT Instability (FMCAD paper)
Zhou et al. (2023)
The Silent (R)evolution of SAT
Fichte et al. (2023)
Proof Assistance and Repair in Crux
Scott (2023)
Making a Scalable SMT-based Machine Code Memory Model
Scott (2023)
A User Study for Evaluation of Formal Verification Results at Bosch
Kaleeswaran et al. (2023)
Going Beyond an Incident Report with TLA+
Hackett (2023)
Formal Methods Only Solve Half My Problems
Brooker (2022)
The Verification Gap
Weisberger (2022)
Finding and Understanding Incompleteness Bugs in SMT Solvers
Bringolf, Winterer, Su (2022)
A Billion SMT Queries a Day
Rungta (2022)
Getting into Formal Specification
Brooker (2022)
Building a Concurrency Verifier Using Crucible
Bakst, Dodds (2021)
Breaking Aave Upgradeability
Feist (2020)
Towards Making Formal Methods Normal
Reid et al. (2020)
Validating SMT Solvers via Semantic Fusion
Winterer et al. (2020)
Generating Crosswords via SAT/SMT
Bohlender (2020)
Spatial Layout of Procedural Dungeons Using Linear Constraints
Whitehead (2020)
Scaling Static Analyses at Facebook
Distefano, O'Hearn et al. (2019)
I Test in Prod
Majors (2019)
The Business Case for Formal Methods
Wayne (2019)
Why Don't People Use Formal Methods?
Wayne (2019)
Programming Z3
Bjørner et al. (2019)
Refutation-Based Synthesis in SMT
Reynolds et al. (2019)
SMT-based Reasoning About the Fast Inverse Square Root
Bohlender (2019)
Solving a Logic Synthesis Puzzle via SAT/SMT
Bohlender (2019)
Modern SAT Solvers Part 3
Hořeňovský (2019)
Alloy: A Language and Tool for Exploring Software Designs
Jackson (2019)
Modern SAT Solvers: Fast, Neat and Underused
Horenovsky (2018)
Lessons from Building Static Analysis Tools at Google
Sadowski et al. (2018)
Bonsai: Synthesis-Based Reasoning for Type Systems
Chandra, Bodík (2018)
Building a Program Synthesizer
Bornholt (2018)
Can You Train a Neural Network Using an SMT Solver?
Bornholt (2018)
Modern SAT Solvers Part 2
Hořeňovský (2018)
Automated Reasoning and Amazon s2n
AWS (2017)
Correctness of Formally Verified Distributed Systems
Fonseca et al. (2017)
A General Approach to Network Configuration Verification
Beckett et al. (2017)
Cosette: An Automated Prover for SQL
Chu et al. (2017)
Souper: A Synthesizing Superoptimizer
Sasnauskas et al. (2017)
SpaceSearch: A Library for Building and Verifying Solver-Aided Tools
Weitz et al. (2017)
Abstracting the Geniuses Away from Failure Testing
Alvaro, Tymon (2017)
Software Verification: Testing vs. Model Checking
Beyer (2017)
Formal Verification: Will the Seedling Ever Flower?
White (2017)
Growing a Protocol
Ramasubramanian et al. (2017)
Chaos Engineering
Basiri et al. (2016)
Experiences with QuickCheck: Testing the Hard Stuff
Hughes (2016)
The Verification of a Distributed System
McCaffrey (2016)
Viper: A Verification Infrastructure for Permission-Based Reasoning
Müller, Schwerhoff, Summers (2016)
Scalable Verification of BGP Configurations with an SMT Solver
Weitz et al. (2016)
Specifying and Checking File System Crash-Consistency Models (Ferrite)
Bornholt et al. (2016)
Who Builds a House Without Drawing Blueprints?
Lamport (2015)
How Amazon Web Services Uses Formal Methods
Newcombe et al. (2015)
Alive: Automatic Verification of Peephole Optimizations in LLVM
Lopes et al. (2015)
Deconstructing Dynamic Symbolic Execution
Ball, Daniel (2015)
One Week of Bugs
Luu (2014)
Testing vs. Informal Reasoning
Luu (2014)
This World of Ours
Mickens (2014)
SMACK: Decoupling Source Language Details from Verifier Implementations
Rakamarić, Emmi (2014)
A Candid Industrial Evaluation of Formal Software Verification Using Model Checking
Bennion et al. (2014)
Productivity for Proof Engineering
Staples et al. (2014)
Syntax-Guided Synthesis
Alur et al. (2013)
Why3: Where Programs Meet Provers
Filliâtre, Paskevich (2013)
SemFix: Program Repair via Semantic Analysis
Nguyen et al. (2013)
Program Sketching
Solar-Lezama (2013)
Growing Solver-Aided Languages with Rosette
Torlak, Bodik (2013)
Testing or Formal Verification: DO-178C Alternatives and Industrial Experience
Moy et al. (2013)
How Does Formal Verification Affect Software Testing?
Regehr (2012)
When Will Software Verification Matter?
Regehr (2012)
Software Synthesis Procedures
Kuncak et al. (2012)
Corral: A Solver for Reachability Modulo Theories
Lal, Qadeer, Lahiri (2012)
SAGE: Whitebox Fuzzing For Security Testing
Godefroid, Levin, Molnar (2012)
Large-Scale Formal Verification in Practice: A Process Perspective
Andronick et al. (2012)
A Decade of Software Model Checking with SLAM
Ball, Rajamani (2011)
In-Depth: Static Code Analysis
Carmack (2011)
Satisfiability Modulo Theories: Introduction and Applications
de Moura, Bjørner (2011)
Synthesis of Loop-Free Programs
Gulwani et al. (2011)
Bug-Assist: Assisting Fault Localization in ANSI-C Programs
Jose, Majumdar (2011)
Answer Set Programming for Procedural Content Generation
Smith, Mateas (2011)
Really Rethinking Formal Methods
Parnas (2010)
Dafny: An Automatic Program Verifier for Functional Correctness
Leino (2010)
Formal Methods: Practice and Experience
Woodcock et al. (2009)
Bounded Model Checking of Software Using SMT Solvers
Armando, Mantovani, Platania (2009)
KLEE: Unassisted and Automatic Generation of High-Coverage Tests
Cadar, Dunbar, Engler (2008)
Z3: An Efficient SMT Solver
de Moura, Bjørner (2008)
Efficient E-Matching for SMT Solvers
de Moura, Bjørner (2007)
MiniZinc: Towards a Standard CP Modelling Language
Nethercote et al. (2007)
Kodkod: A Relational Model Finder
Torlak, Jackson (2007)
The Power of Ten
Holzmann (2006)
The Future of Computing: Logic or Biology
Lamport (2006)
A Fast Linear-Arithmetic Solver for DPLL(T)
Dutertre, de Moura (2006)
Translating Pseudo-Boolean Constraints into SAT
Eén, Sörensson (2006)
Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
Sinz (2005)
An Extensible SAT-solver (MiniSat)
Eén, Sörensson (2004)
DPLL(T): Fast Decision Procedures
Ganzinger et al. (2004)
Chaff: Engineering an Efficient SAT Solver
Moskewicz et al. (2001)
Is Proof More Cost-Effective Than Testing?
King et al. (2000)
Security in the Real World
Schneier (1999)
Acceptance of FM: Lessons from Hardware Design
Dill, Rushby (1996)
How Did Software Get So Reliable Without Proof?
Hoare (1996)
The Rise of Worse is Better
Gabriel (1991)
Program Verification: The Very Idea
Fetzer (1988)
No Silver Bullet
Brooks (1986)
Programming as Theory Building
Naur (1985)
Reflections on Trusting Trust
Thompson (1984)
Social Processes and Proofs of Theorems and Programs
DeMillo, Lipton, Perlis (1979)
The Humble Programmer
Dijkstra (1972)