1 of 10 · The problem

The wrong-spec problem

An agent can build exactly what it was told, and still build the wrong thing.

An agent is an AI that does the work, such as Claude Code. A spec is what it builds from: the request, the ticket, and the tests.

Wrong

The spec does not match how things really are.

Incomplete

The spec leaves out a case that matters.

Read two ways

The human and the agent read the same words and see different things.

The human is the source of intent. The human is not always the source of clarity.

Full deck: the wrong-spec problem

2 of 10 · The problem

"Make the button purple"

The agent built what it understood. The test checked what the agent understood. Only the human saw the gap, and only at the end.

The fix costs one line, if it comes early. The agent says its claim back with one example, and the human answers: No, only that button.

Full deck: the example

3 of 10 · The idea

Alignment

The human, the agent, and the formal records agree on what to build and on when it is done.

No one grades their own work. The human verifies the result, not the test results.

Clear
Accurate
Honest
Fast

Full deck: the philosophy, the roles, and loud versus quiet

4 of 10 · The idea

Tests and proofs

The real claim behind "add discount codes": no discount code takes a price below the floor, for every code and every cart.

A test shows a claim for the cases that it tries. A proof shows it for all cases of the model.

A test written from a wrong spec passes.

So ask early whether the spec matches what the human means. When a claim must hold for every case, prove it in Lean.

Full deck: tests and proofs

5 of 10 · The story

The idea held; the machinery changed

The author, Ty, reached this process in 2026 through three eras. The process kept changing. The delivery did not.

The philosophy held the whole way, so the quality of the client work held. What changed was how much of the method a tool ran.

Full deck: the timeline, the five chapters, and the eras

6 of 10 · The story

Why signals, not tiers

The AIDLC, the era before, sorted work into tiers by difficulty. The middle tiers drifted to the ends, and what is hard for a model changes with every model. One thing does not change:

People change their minds, and often don't know what they want until they see it. Better models will guess better, but not every time, and least of all on the niche asks.

"I'm making the bet that even with ASI, humans will still need to explain what they want."

Full deck: why the tiers had to go

7 of 10 · The tool

What it is

The prompt tells the agent how to work. orbit-kb keeps the records honest: every fact is declared, typed, and checked.

The prompt: One plain-text file, appended to the agent's system prompt. It says how to work: start light, shift up on a signal.
orbit-kb: A command-line tool that keeps the knowledge base (KB): every fact declared, typed, and checked.
Prolog: SWI-Prolog 9 or later: answers the KB's questions.
Lean 4: Only for proofs. Install with elan. Optional helpers: sharlean (shared libraries such as Mathlib) and lean-lsp-mcp.

Full deck: what it is, and why Lean and Prolog

8 of 10 · The tool

How to use it

Two setup steps, then three steps for each request. The human's part is to ask, answer, and verify.

You rarely type orbit-kb yourself. Most requests stay on the light path: one check, no KB.

Install on Fedora

On another system, use its package manager for SWI-Prolog 9 or later, then follow the same steps.

$ sudo dnf install swi-prolog-nox
$ orbit-kb doctor

For orbit-kb prove, install Lean 4 and Lake with elan. A Lean project that needs Mathlib builds it slowly. If you have several such projects, you can share one built copy of the libraries between them. In the sagittarius repo, ./install.py puts orbit-kb on the PATH and its rules in ~/.local/share/orbit-kb.

Full deck: how to use it, with the commands the agent runs

9 of 10 · In practice

The gradient

No tier is picked up front. Each signal adds one rung, and each rung comes off when its cause is resolved.

Fixed tiers had no middle. Here each trigger adds only its own rung, in any order: a universal claim can burn with no questions asked.

"This pattern offers, when it really needs it, a level of rigor that can guarantee correctness."

A proof holds for every case of the Lean model. The checks tie the model to the code.

The lightest path, step by step · The most rigorous path

10 of 10 · In practice

What you get back

Six fields, in short plain sentences. An empty field says "none", so you see that the agent looked.

Delivered:    Submit on /checkout is purple.
Claims:       Submit on /checkout renders #6B3FA0: fulfilled (check red, then green).
Guesses:      Only this button, not every primary button.
Disclosures:  none
Not checked:  dark mode
To land:      none; merged.
Screenshot attached. No KB.

Go deeper

Without JavaScript, scroll.