This path supports a talk on formal methods a working engineer can adopt. The core is property-based testing, small model checking, types as specs and contracts. Coding agents change what formality costs, so the talk also asks what that shift means. The path runs from why now to specs, cheap checks and specs in code. A short last stage covers the heavy foundations, only where they explain the light practice.
1. Why is formality worth another look now?
The bookmarks argue that agents change what formal methods cost and return. Start here for the talk's opening claim.
- Formal methods and the future of programming: Minsky says Jane Street long judged formal methods too costly. The post argues agentic coding lowers that cost and makes verification the bottleneck.
- The Case Against Formal Verification, 50 Years Later: Gavran re-reads six arguments from a 1979 paper against verification. It gives the talk the classic objections and a practitioner's answer to each.
- Treat Agent Output Like Compiler Output: Nobody reads compiler output, the post says, because tests, types and fuzzing back it. It lists formal specs among the apparatus agents still lack.
2. What is a spec an engineer can actually check?
Before tools, the talk needs a working definition of a spec. These sources argue about how precise, how short and who writes it.
- A spec the agent can't run isn't a spec yet: Lewis argues executability matters more than format. A check written beforehand, which the agent cannot edit, sits outside the loop.
- A sufficiently detailed spec is code: Gonzalez argues a spec precise enough to generate code becomes code. One Haskell trial from a prose spec produced several bugs. It targets specs replacing code, not checks testing it.
- DSLs Enable Reliable Use of LLMs: Joshi argues a small language's compiler lets an agent check and repair alone. Illegal sequences can fail to compile.
- Human Judgment as a Specification: PICK shows people concrete cases where candidate specs disagree, and they vote. It answers how vague intent becomes a formal spec without a person rubber-stamping.
3. How do cheap checks find real bugs?
This is the core of lightweight practice: random properties and small models. The bookmarks have one strong model-checking story and one study of property testing.
- Hunting a 16-year-old SQLite bug with TLA+: is dqlite affected?: Two actions and one invariant found SQLite's WAL bug in 20 states. A second model showed dqlite cannot hit it. This is the talk's best worked example.
- On the Unreasonable Effectiveness of Property-Based Testing for Validating Formal Specifications: Feng and Sergey use random tests to check specs themselves. About 10% of benchmark specs tested were underspecified. Testing can refute a spec but not prove it.
- Linearizability! Refinement! Prophecy!: Hochstein builds TLA+ from a counter up to a queue, for beginners. It frames a spec as a state machine. Its later sections show where model checking turns heavy.
4. How do types and contracts carry the spec inside everyday code?
Here the spec lives in the language, checked on every build. These sources show it at work in Go, Haskell and an operating system language.
- Structural Backpressure Beats Smarter Agents: Brooks separates prompt rules from compiler and type gates. One demo turns a spec into Go guard types for tenant access. The post names the costs too.
- Haskell koan: Type-checked non-empty strings: A production trick rejects empty string literals at compile time. It is a small, concrete case of a type as a spec.
- The Error Model: Duffy describes Midori's
requirespreconditions replacing most argument-checking exceptions. It is the pile's main source on contracts in a real language.
5. Where does it come from, when the talk needs foundations?
Keep this stage short in the talk. These sources explain why a contract or invariant works, without making proof the goal.
- Lecture Notes: Hoare Logic: The notes treat a specification as a contract with callers. They link contracts, invariants and termination in a few pages.
- Hoare2: Hoare Logic, Part II: The chapter says finding loop invariants is the only creative part. Its worked failed guesses show what an invariant is for.
- The hitchhiker's guide to reading Lean 4 theorems: The post teaches programmers to read theorems as typed code. It warns the kernel checks what was stated, not what was meant.
Also in the wiki
- How we tracked down a 16-year-old SQLite bug: the production side of the TLA+ story.
- What can you confidently guarantee about your software?: practitioners on proofs, model checking and property testing.
- Understanding Spec-Driven-Development: Kiro, spec-kit, and Tessl: trials of spec-driven agent tools.
- On the foolishness of "natural language programming" (EWD 667): Dijkstra on why formal symbols help.
- Your job is to deliver code you have proven to work: a test that fails if the change is reverted.
- Vibe Coding: test the tests, since agents pass weak ones.
- Thermite: mandatory contracts with an assurance ladder.
- Evolving programming languages in the AI era: agents may favour stronger guarantees.
- A Whirlwind Tour - SpecForge User Guide: temporal specs, monitoring and falsification.
- I rewrote PostHog's SQL parser, 70x faster, while barely looking at the code: old parser kept as a checking oracle.
- How much can you delegate to agents?: easy-to-check work earns autonomy.
- Immutable Infrastructure, Immutable Code: specs and evaluations as the lasting asset.
- Towards a Theory of Bugs: The Ruliology of the Unexpected: rare bugs that sampling misses.
- Your type checker may be wrong - an introduction to formal proof verification and the Curry-Howard Correspondence: Curry-Howard for programmers.
- A Lean Syntax Primer: a theorem as a test for all inputs.
- Tutorial: Introduction to Formal Verification with Lean (Part 1): one-time pad proved correct.
- Theorems for Free!: theorems from types alone (thin entry).
- Satisfiability modulo theories - Wikipedia: the solvers behind many checkers.
- Hoare: Hoare Logic, Part I, Refinement Calculus Tutorial, On the Refinement Calculus: the heavy end.
- AeneasVerif/aeneas: A verification toolchain for Rust programs: Rust to proof assistants.
- Everyone Says Assembly Is Untyped - Everyone Is Wrong: types checked even on assembly.
Probably missing
- Stage 1 lacks the source that named the field. Candidate: Jackson and Wing, "Lightweight Formal Methods", IEEE Computer, 1996, https://doi.org/10.1109/MC.1996.10038. Not in the bookmarks.
- Stages 1 and 3 lack an industry report on return. Candidate: Newcombe et al., "How Amazon Web Services Uses Formal Methods", CACM 2015, https://www.amazon.science/publications/how-amazon-web-services-uses-formal-methods. Not in the bookmarks.
- Stage 3 has no practical property-based testing guide for mainstream code. Candidate: Hypothesis documentation, https://hypothesis.readthedocs.io/. Not in the bookmarks.
- Stage 3 has no beginner TLA+ course. Candidate: Hillel Wayne, Learn TLA+, https://learntla.com/. Not in the bookmarks.
- Stage 3 has no Alloy. The one "Alloy" bookmark is an unrelated ORM. Candidate: Alloy tools and books, https://alloytools.org/book.html. Not in the bookmarks.
- Stage 4 lacks the everyday types-as-specs essay. Candidate: Alexis King, "Parse, don't validate", https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-validate/. Not in the bookmarks.
- Stage 4 has contracts only as history. A checked-contracts language would fill it. Candidate: Dafny, https://dafny.org/. Not in the bookmarks.
Caveats
- The heavy end is well stocked: Hoare logic, refinement calculus, Lean, Rocq. The light practice is thin: no Alloy, no hands-on property testing, one TLA+ case.
- Gonzalez and Fowler pull in opposite directions. Fowler treats the spec as the asset. Gonzalez says a full spec becomes code. Lewis and Joshi offer a middle: small executable checks.
- Most "why now" sources are argument from interested parties. Minsky is hiring, SkipLabs and Brooks sell tools. None measures agents with formal methods.
- Feng and Sergey give the one number: about 10% of tested specs were underspecified. It covers Lean benchmarks only.
- Contracts rest on Duffy alone. Midori never shipped, so pair it with a living tool.