Write down every guarantee before you write any code

Here is every promise a to-do list makes. VARIABLE tasks Init == tasks = [i \in Ids |-> "absent"] Add(i) == tasks[i] = "absent" /\ tasks' = [tasks EXCEPT ![i] = "open"] Complete(i) == tasks[i] = "open" /\ tasks' = [tasks EXCEPT ![i] = "done"] Reopen(i) == tasks[i] = "done" /\ tasks' = [tasks EXCEPT ![i] = "open"] Delete(i) == tasks[i] # "absent" /\ tasks' = [tasks EXCEPT ![i] = "absent"] ClearCompleted == /\ \E i \in Ids : tasks[i] = "done" /\ tasks' = [i \in Ids |-> IF tasks[i] = "done" THEN "absent" ELSE tasks[i]] 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. Now go find that list for the system you work on. 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. The prime mark and two operators That's most of the syntax, so let's get it out of the way. 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. That's it. That's the language, near enough, for this purpose. The real file 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 == / \E i \in Ids : Add(i) / Complete(i) / Reopen(i) / Delete(i) / ClearCompleted Spec == Init /\ [][Next]_tasks 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. The list is short, finite, and worth arguing about The objection I expect is that a real system's list would be enormous. 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, 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, the language and tools got a book in 2002, and Lamport picked up the 2013 Turing Award 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. What changed 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. tlatools-rs cargo install tlatools A TLA+ parser and evaluator in Rust. Not a model checker - it doesn't explore anything. It answers questions about states you already have: let spec = Spec::from_file("Todo.tla")?; let eval = Evaluator::new(&spec, constants)?; eval.holds_at("Init", &state)?; // legal starting state? eval.step_allowed("Next", &from, &to)?; // legal step? The loop is three pieces. You write the list - short, arguable, and it barely changes. The agent writes the implementation - any language, any framework, any speed. A script walks the implementation and asks the list about every step it takes. That third piece is thirty lines: ask the implementation what it can do, do each of those things, record where you landed, repeat until nothing new turns up. $ ./check.py impl/correct.py The implementation refines the specification. 9 states and 35 steps, all permitted. Nine states because there are two tasks and three states each. A real app has more, and the walk is the expensive part, not the checking. Two bugs the list catches Here's an agent-plausible one. The completion handler takes an id and marks it done. It doesn't check the task was open - why would it, the button only shows up on open tasks. (The button. Not the handler.) This is exactly the bug that survives review. It reads correctly. The missing check is missing somewhere you aren't looking. $ ./check.py impl/completes_anything.py The implementation takes a step the specification does not permit. from a=absent, b=absent doing complete(a) to a=done, b=absent The closest the specification came: Add(i = "a") was available, but does not produce that state, because tasks' = [tasks EXCEPT ![i] = Open] does not hold (1 of its 2 clauses hold) Complete(i = "a") was not available here, because tasks[i] = Open does not hold (1 of its 2 clauses hold) The second line is the bug, named: Complete requires the task to be open, and it wasn't. It's a ranked shortlist rather than a single guess - Add also nearly fits from this state, and saying so is more honest than pretending to know which one you meant. Now the other one. ClearCompleted - the action with two promises. This implementation keeps the first and breaks the second. It clears the whole list: $ ./check.py impl/clear_removes_everything.py from a=open, b=done doing clear_completed to a=absent, b=absent The closest the specification came: ClearCompleted was available, but does not produce that state, because tasks' = [i \in Ids |-> IF tasks[i] = Done THEN Absent ELSE tasks[i]] does not hold (1 of its 2 clauses hold) "Was not available here" versus "was available, but does not produce that state." Different sentences because they're different bugs. One is a missing guard. The other is a correct guard and a wrong effect - which is worse, because the button looks like it works. You'd demo it. You'd ship it. Someone would lose a task they hadn't finished. The tool can tell them apart because it knows which failing clause mentions the next state. Neither bug is exotic. Both are invisible to a test suite that checks outcomes, and both are named instantly by a list you wrote in nine lines. Feedback in the language the rule was written in You cannot fix what you cannot describe, and neither can a model. - "Tests failed." - Try again. Randomly. - "Expected {a: open} , got{a: absent} ." - Better. Now infer the rule. - " ClearCompleted was available, but does not produce that state, becausetasks' = [i \in Ids |-> IF tasks[i] = Done THEN Absent ELSE tasks[i]] does not hold." - The action, the condition, and the state it was in. That third one is a prompt. And I measured whether it helps an agent, and it didn't - not detectably. 200 tasks, each attempted with an uninformative retry and with the failure text fed back: 90.5% [85.6-93.8] against 92.5% [88.0-95.4], McNemar exact p=0.125. That is a null. On the formal-reasoning subset the gap was 46.2% → 69.2%, which looks like something, except n=13 and p=0.25, which means it looks like something in the way small numbers often do. I'm reporting it because I ran it. The honest state of the claim: the mechanism is sound, the message is strictly more information than a boolean, and I have no evidence it moves the pass rate. If you were going to adopt this because "agents do better with good errors" - don't, yet. Adopt it because you now have the list, and something checks it. The list as a grader tlatools check takes a JSON job - spec, states, steps, const