Not a summary. Not the important ones. All of them. A task cannot go from absent straight to done. Clearing completed items leaves the open ones alone. You cannot delete something that was never there. Nine lines, and when you've read them you have read the entire contract.
You can't. It doesn't exist. It's distributed across a test suite that asserts outcomes rather than rules, some validation scattered through handlers, and the memory of whoever's been there longest. The guarantees are real — your users depend on every one of them — and there is no file you can open to see them.
That's the gap I want to talk about, because you can close it in an afternoon, and because something has changed recently that makes closing it pay for itself.
tasks' means "tasks, in the next state." /\ is and. \E is "there exists." A definition like Complete(i) is a formula relating the current state to the next one — read it out loud: the task is open, and afterwards it is done.
[The real file][demo] adds about eight lines of scaffolding around what you saw: a module header, a TypeOK saying a task is always in exactly one of the three states, and the two lines that tie the actions together —
Next is "any one of the moves happens." Spec is "start legally, and then only ever make legal moves." That second line turns out to matter more than it looks, and I'll come back to it.
Notice what isn't in there. No database. No HTTP. No mention of whether the button is blue or whether completion is optimistic in the UI. A specification isn't a program and doesn't compile to one — it's a formula that says which state changes are permitted. Everything else is out of scope by construction, which is exactly why the list can be nine lines and still be complete.
And notice ClearCompleted has two halves: the button only exists when something is done, and it leaves everything else alone. Two separate promises in one action. Hold that thought.
It's smaller than you think, because it's a list of rules, not behaviours. The behaviours are combinatorial — nine states here, and a real system has astronomically many. The rules that generate them are not. Five actions cover every to-do list that has ever been correct.
It's also the part of the design worth arguing about. When two engineers disagree about whether reopening a completed task should be allowed, that argument currently happens in a code review, in a comment thread, three weeks after someone already built one of the answers. Written as a spec, the argument takes four minutes and happens before anyone opens an editor.
That's the [AWS result][aws], really. They wrote up their experience in CACM in 2015 and the headline everyone quotes is about proving systems correct. The part that actually replicates is quieter: writing the spec found bugs before any code existed — in systems their best engineers had already designed and reviewed. Not bugs the tests missed. Bugs the design had, findable by writing the guarantees down and reading them back.
This is forty-year-old technology, and most of us skipped it because it looked like homework. TLA+ is Leslie Lamport's; the temporal logic underneath it landed in [TOPLAS in 1994][toplas], the language and tools got a [book in 2002][book], and Lamport picked up the [2013 Turing Award][turing] along the way. (Not for TLA+, worth saying, since people get this wrong: the citation is logical clocks, safety and liveness, replicated state machines, sequential consistency. TLA+ is downstream of that work, not the reason for the medal.)
Its reputation for being academic is partly earned and mostly out of date. You do not need the proof system. You do not need to verify anything. You need the part where you write the guarantees down.
Writing the list has always been worth it and has always been easy to defer, because the code was going to be written slowly by people who mostly remembered the rules.
That is no longer the situation. Something else is writing the code now, quickly, and it does not remember anything. It has never met your system's rules and has no way to infer the ones that aren't in the file it's looking at. It will write something plausible.
Plausible is the problem. Plausible code passes review — this is where "looks good to me" comes from, and it was always an honest confession: the reviewer is reporting that nothing jumped out, because checking against the full set of invariants was never an option. Nobody had the list.
So: write the list. Then check the generated code against it, mechanically, every time. That second half needs a tool.
A TLA+ parser and evaluator in Rust. Not a model checker — it doesn't explore anything. It answers questions about states you already have: