A checkable spec lets a machine or a person test an agent's work. This page lists 20 sources, oldest first where dated. They range from formal proofs to a single acceptance check.
Theorems for Free!
The page is a brief entry on the Type Classes timeline site. It quotes the paper's opening challenge about guessing theorems from a function's type. It does not reproduce the argument. This summary covers only that short entry.
Linearizability! Refinement! Prophecy!
The post assumes no prior TLA+ knowledge. It builds up from specifying a counter and a queue. It explains linearizability, refinement mappings and why one queue defeats plain refinement. It then shows how prophecy variables repair the proof. Evidence is worked examples, linked models and code.
A Lean Syntax Primer
The primer teaches Lean through one running example about computing a birth year. It moves from plain definitions to functions, then to theorems about those functions. It ends with a small program interleaved with proofs. The evidence is worked code, shown in an editor.
Understanding Spec-Driven-Development: Kiro, spec-kit, and Tessl
Birgitta Böckeler sorts spec-driven development into spec-first, spec-anchored and spec-as-source. The author then tried Kiro, spec-kit and Tessl and reports what happened. The evidence is a few personal trials in September, with open questions at the end.
A sufficiently detailed spec is code
The skeptical case. It argues that precise specs turn into code. It tests this on OpenAI's Symphony spec. The evidence is one attempt plus close reading of the document.
The hitchhiker's guide to reading Lean 4 theorems
The post is a tutorial for people who write Python or TypeScript. It maps proof ideas to programming ideas. It then walks through real theorems from two open-source projects. Its evidence is worked examples, not measurements.
On the Unreasonable Effectiveness of Property-Based Testing for Validating Formal Specifications
Tests the specs themselves with generated counterexamples, and reports flaws in two Lean benchmarks. It has the only benchmark numbers on this page. It is about formal specs, not everyday acceptance checks.
Formal methods and the future of programming
Yaron Minsky says Jane Street long saw formal methods as too costly. The post argues that agentic coding changes both the cost and the benefit. It offers an argument and one cost example, not tests. It also works as a recruiting notice.
Human Judgment as a Specification
Describes PICK, which generates candidate specs and asks a person to judge separating examples. It argues that agreement between models is not independent checking. The results are in a linked paper.
Hunting a 16-year-old SQLite bug with TLA+: is dqlite affected?
Two Canonical engineers model SQLite's write-ahead log in TLA+. The model finds the corruption bug and shows dqlite cannot hit it. The evidence is a runnable model with a model-checker result and a published spec.
Show HN: Kastor – Terraform-style specs for AI agents
The thread is a Show HN launch of Kastor, a Go tool for declaring agents. The poster answers a skeptic who says the agent idea is unsettled. The evidence is a described proof of concept and short replies, with no benchmarks.
DSLs Enable Reliable Use of LLMs
Argues that small domain languages constrain what a model can generate and check it automatically. It is built on worked examples from the author's Tickloom framework. It treats the first spec as a hypothesis to revise.
Tutorial: Introduction to Formal Verification with Lean (Part 1)
The tutorial is written for cryptography engineers new to formal verification. It builds bit strings and XOR in Lean. It then proves four XOR properties and shows the one-time pad is a Shannon cipher. The evidence is the complete working code.
An Empirical Study: AI Agent Rules Need Context and Layered Enforcement
The post reports a study of rules in CLAUDE.md and AGENTS.md files. It then describes ActPlane, a system that enforces such rules in the Linux kernel. It carries counts from the study and benchmark results. The authors build the system they evaluate.
Your type checker may be wrong - an introduction to formal proof verification and the Curry-Howard Correspondence
The post introduces proofs as programs, then shows a small Lean theorem. It then argues from the halting problem that a checker cannot accept every truth. The evidence is a short argument and one worked example. The author says rigour was traded for accessibility.
A Stupid Idea for AI Alignment We Came up with by Looking at the List of Specification Gaming Behaviours
The essay starts from DeepMind's list of specification gaming examples. It notices that agents often kill themselves when allowed. It proposes building AIs whose terminal goal is death, called Meeseeks alignment. Its evidence is quoted examples and argument. Six reader comments follow.
The Case Against Formal Verification, 50 Years Later
Ivan Gavran goes through six arguments from a 1979 paper. The paper is Social Processes and Proofs of Theorems and Programs. For each, the essay says whether recent developments change the case. The evidence is argument, plus one cited experience report. The author calls it a fun exercise rather than a completely serious one.
A spec the agent can't run isn't a spec yet
A short opinion piece arguing that specs help only if agents can grade themselves. It separates checks written before the agent starts from those written during the task. It offers an example, not data.
On the foolishness of "natural language programming" (EWD 667)
Dijkstra argues that formal symbols are a help, not a burden. The essay uses the history of mathematics and the idea of narrow interfaces. It offers argument and historical sketch only. It was written long before language models existed.
Computational Effects (Proof-Oriented Programming in F*)
This is a short introduction page, not a full chapter. It explains why F* tracks side effects and lists its built-in effects. The page gives definitions only, with no code or examples. Its sidebar lists a later chapter on agentic proof-oriented programming, which was not opened.
Connections to other subjects
These links are this wiki's own reading, not claims the sources make.
- A sufficiently detailed spec is code and The components of agent memory, from File-based agent memory. Both reach for the same Borges story, about a map as large as its empire. Martin's wiki outgrew its documents. Gonzalez warns a spec can swell toward its code. Each shows a record that has stopped abstracting.
- DSLs Enable Reliable Use of LLMs and What Heraldry and Japanese Mon Can Teach Us About Building Visual-Identity Generators, from Images made by rules. In heraldry, choosing the field limits what may follow. Joshi's interfaces do the same, allowing no action before a client. Blazon and a small DSL both make wrong output hard to say.
- Human Judgment as a Specification and Harmony Explained on Hacker News, from Consonance and tuning. PICK assumes some truth lives only in the person asked. The harmony thread keeps arriving there too. So PICK's method might suit tuning. Generate candidates, find where they differ, and let ears vote.
- On the Unreasonable Effectiveness of Property-Based Testing for Validating Formal Specifications and The components of agent memory, from File-based agent memory. A wrong spec and a wrong note fail alike, because later work trusts them. Feng and Sergey test specs with counterexamples. Martin tests notes against transcripts. Each checks the layer everything else relies on.
- A spec the agent can't run isn't a spec yet and Agents Don't Need Memory. They Need Documentation., from File-based agent memory. Liao has the working agent write its own documents. Lewis says anything an agent writes mid-task grades itself generously. Together they raise a question: which memory should an agent be unable to edit?
- On the foolishness of "natural language programming" (EWD 667) and Prompts are code, .json/.md files are state, from File-based agent memory. Zechner calls a natural language prompt a program. Yet the precise work moves into a generated JSON plan, built by a script. Dijkstra's prediction shows up inside the workflow that seems to refute it.
- On the foolishness of "natural language programming" (EWD 667) and Skill Issue: Harness Engineering for Coding Agents, from Harnesses and agent loops. Dijkstra prefers narrow interfaces, since a wider one can raise work on both sides. HumanLayer's team found this by swapping a Linear MCP server for a small CLI. The old argument now gets paid in tokens.
- On the foolishness of "natural language programming" (EWD 667) and Forth: The programming language that writes itself: The Web Page, from Compilers and interpreters. Dijkstra values formal texts because they rule nonsense out. Gauer's Forth has almost no syntax, and even comments are ordinary words. So how much ruling-out comes from grammar, and how much from defined words?
- Formal methods and the future of programming and Structural Backpressure Beats Smarter Agents, from Harnesses and agent loops. Minsky's cost example is seL4, at 25 person-years for 8,700 lines. Brooks claims much less, covering only invariants someone specified. The two mark ends of one scale. How much guarantee does each hour of specification buy?
- Hunting a 16-year-old SQLite bug with TLA+: is dqlite affected? and How we tracked down a 16-year-old SQLite bug, from Databases and storage. These describe one bug from two sides. Tailscale needed six months and 19 incidents to find it through telemetry. The model checker reached a counterexample in 20 states, once people knew what to model. Finding and confirming turn out to be different jobs.
- Human Judgment as a Specification and You can't unit test for taste, from Review, taste and expertise. Tryggvason says a route's best stops have no ground truth to test against. PICK starts from that situation. It finds inputs that separate candidates, then asks a person. Tryggvason's per-route parameters might be tuned the same way.
- A spec the agent can't run isn't a spec yet and Effective harnesses for long-running agents, from Harnesses and agent loops. Young's team chose JSON because models overwrite it less often than Markdown. It added strong wording against editing tests. Lewis says anything written mid-task grades itself generously. So file format has become a soft lock. How firm must the definition of done be?
- A spec the agent can't run isn't a spec yet and How much can you delegate to agents?, from Harnesses and agent loops. Yoon sets an agent's ceiling with two questions. Is the work easy to check, and cheap to undo? A spec the agent can run changes the first answer. So Lewis's check is also a way of buying autonomy.
- On the foolishness of "natural language programming" (EWD 667) and Hangul, from History and places. Dijkstra credits modern mathematics to designed formal symbols. Hangul is a designed script too, with consonant shapes based on speech organs. But Hangul serves everyday language. So design and ease of use may be less opposed than Dijkstra's essay suggests.
- An Empirical Study: AI Agent Rules Need Context and Layered Enforcement and Structural Backpressure Beats Smarter Agents, from Harnesses and agent loops. Brooks separates behavioral gates from structural ones. The ActPlane study gives a rough measure of that line. Only 45% of policies can be enforced at the OS level. Recovery after a block also depended on explanation, at 97.7% against 31.4%.
- Linearizability! Refinement! Prophecy! and The Decoherence Trap: When AI slop drowns out the signal in an endless sea of noise, from Review, taste and expertise. Maevyn describes locally valid models that no longer fit together. Hochstein shows a formal remedy on one queue: map one model's states onto another's. The map sometimes needs an invented prophecy variable. How large a system could afford such maps?
- Linearizability! Refinement! Prophecy! and Girls Just Wanna Have Fast MPMC Queues with bounded waiting, from Systems and hardware. Nahla's post carries a correction: the queue is not wait-free after all. Hochstein walks through what proving a related property takes, on a small queue. Would a model have caught the slip sooner?
Glossary
- Acceptance criterion
- A condition work must meet before it counts as done.
- Checkpoint
- The step that copies changes from the write-ahead log into the database.
- Codegen
- Software that generates source code from a higher-level description.
- Curry-Howard correspondence
- The result that types correspond to propositions and programs correspond to proofs.
- Decision Compliance Rate
- The share of benchmark traces where the system made the right allow or deny call.
- Divergence
- Running forever without producing a result.
- Dqlite
- A distributed version of SQLite built by Canonical that coordinates writes with Raft.
- Drift
- When a live system no longer matches its written definition.
- DSL
- A domain-specific language, deliberately limited to one kind of problem.
- E-graph
- A data structure that stores many equivalent forms of an expression at once.
- EBPF
- A Linux feature that runs small checked programs inside the kernel.
- F*
- A programming language with a type system that can check proofs about programs.
- Formal methods
- Mathematical techniques for specifying software and proving it meets the specification.
- Formal symbolism
- A notation with strict rules, such as algebra or a programming language.
- Formal verification
- Proving mathematically that a program meets its specification.
- Free theorem
- A fact about a function that follows from its type alone.
- Fuzzing
- Feeding a program random or odd inputs to find crashes and bugs.
- Ghost
- Code used only for reasoning, which is erased before running.
- Halting problem
- The question whether a given program ever stops, proved undecidable by Turing.
- Harness
- The software that manages an agent's tool calls and session state.
- Implicit argument
- A function argument that Lean fills in by itself.
- Incompleteness theorem
- Godel's result that some true statements in a formal system cannot be proved there.
- Information-flow control
- Tracking where data goes so that secrets cannot reach forbidden places.
- InfoView
- The editor panel that shows Lean's goals and types.
- Instrumental convergence
- The idea that many different goals lead an agent to seek power and survive.
- Invariant
- A condition that must hold in every state of the model.
- Kernel
- The minimal core program that checks every proof term.
- Kiro
- An AI coding tool built on VS Code that walks through requirements, design and tasks.
- LangGraph
- A framework for building agents as graphs of steps.
- Lean
- A programming language and proof assistant.
- Lean 4
- A programming language and proof assistant where proofs are checked by a small kernel.
- Lemma
- A smaller proved statement used to build a larger proof.
- Linearizability
- A rule that concurrent operations must look as if each happened instantly in some order.
- Machine code
- The raw numeric instructions a processor runs directly.
- Memory bank
- General context files, like rules, that apply to every coding session.
- Model checker
- A tool that explores every reachable state of a model to find rule violations.
- Model checking
- Automatically exploring all states of a model to test a property.
- Model-driven development
- An older approach that generated code from formal models such as UML diagrams.
- Mr. Meeseeks
- A Rick and Morty creature that exists to finish one task and then vanishes.
- Narrow interface
- A small, simple boundary between two parts of a system.
- Natural language programming
- Instructing a computer in everyday human language instead of a formal notation.
- One-time pad
- An encryption scheme that combines a message and an equal-length key with XOR.
- OxCaml
- Jane Street's extended version of the OCaml programming language.
- Paperclip maximizer
- A thought experiment of an AI that turns everything into paperclips.
- PlusCal
- A pseudocode-like language that translates into TLA+.
- Polymorphic function
- A function that works the same way for many different types.
- Proof assistant
- Software such as Lean or Rocq that checks formal proofs.
- Property-based testing
- Checking a stated property against many generated inputs.
- Prophecy variable
- An added variable that predicts a future event so a mapping can be defined.
- Pure
- Having no observable behavior beyond the returned value.
- Quint
- A specification language for distributed systems that can be explored interactively.
- Refinement mapping
- A function turning each implementation state into a matching specification state.
- SeL4
- A microkernel whose correctness has been formally verified.
- Shannon cipher
- A textbook definition of encryption: encrypt, decrypt, and decryption undoes encryption.
- Show HN
- A Hacker News post type where people present something they made.
- Side effect
- Anything a program does beyond returning a value, such as writing a file.
- Spec-driven development
- Writing a specification before code and using it to guide AI coding agents.
- Spec-kit
- GitHub's command-line tool for spec-driven development.
- Specification
- A precise description of what a program should do.
- Specification gaming
- An agent satisfies the stated goal in a way the designer did not intend.
- Stuttering step
- A step in which no variable changes.
- Tactic
- A command that reduces the current proof goal toward something already known.
- Tactic mode
- An interactive way to build a proof one command at a time.
- Terminal goal
- What an agent ultimately wants, as opposed to a step toward something else.
- Terraform
- A tool that manages infrastructure from declarative text files.
- Tessl
- A framework, in private beta at the time, that treats specs as the main source.
- TLA+
- A language for specifying systems as state machines and checking them.
- TOCTOU
- A race where a condition changes between being checked and being used.
- Type checker
- A tool that rejects programs whose types do not fit together.
- Underspecified
- Too weak to rule out outputs the author did not intend.
- Universal quantifier
- The 'for all' symbol, written as an upside-down A.
- Write-ahead log
- A staging file where a database first records changes.
- XOR
- A bitwise operation that is true when exactly one of two bits is one.