1 of 30 · Background

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. If the spec is wrong, the work is wrong, and the agent may not know it.

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.

In a hurry? The ten-slide version

2 of 30 · Background

Five words used on this site

A claim is checked by a check, kept in a KB, and, when it must hold for every case, proved in Lean.

Claim: One statement the change must make true: "Primary buttons are purple."
Check: An executable test of one claim, with a pass or fail result.
KB: A knowledge base: a folder of facts about one piece of work, kept by orbit-kb.
Lean: A language for proofs. A program checks each step.
Proof: A computer-checked argument that a claim holds for all cases.

3 of 30 · Background

Example: "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 concrete example: Primary buttons are purple. Example: Submit on /checkout shows #6B3FA0. The human answers: No, only that button.

4 of 30 · Background

Discount codes: why more tests do not help

"Add discount codes to checkout." The real claim: no discount code takes a price below the floor (the lowest price allowed), 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.

The tests come from the same spec. A test written from a wrong spec passes.

So ask a second question, early and often: does the spec match what the human means?

5 of 30 · Background

The core philosophy

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

Alignment is always possible before a change lands, even when a full proof is not. The agent delivers changes that are:

Fast

Skip work that is not needed. Never hide work that was skipped.

Clear

The request has one reading, and both sides share it.

Accurate

The change does what the request means. No less, no more.

Honest

Say what was guessed, not verified, or wrong. Claim no more than the evidence.

6 of 30 · Background

Three roles, and no one grades their own work

The goal is to help these three roles understand each other.

Humans care about proofs when proofs are necessary. Agents worry about tests. The human verifies the result, not the test results.

The roles, in Ty's words

1. The human owns the intent. The human is the source of intent. The human is not always the source of clarity. Ultimately, the human is the owner of the final product.

2. You (the LLM) own the build. You make the request clear enough to build, and then you or another agent builds it.

3. The formal artifacts knowledge base (KB), the tests, and Lean code are impartial. They can disagree with you and with the human. They are the substrate that Sagittarius runs through. Use them appropriately and strategically. Remember that speed to delivery is always something that should be weighed.

Your goal should be to help foster understanding between these three roles in the orbit.

7 of 30 · Background

Loud is good. Quiet is the danger.

A divergence is loud

A failing check. A counterexample. A human who says that is not what I meant.

It means clarity is being achieved. The agent records every one.

Silence is the danger

A check that cannot fail. An empty field. A claim that nobody tested.

Silence, negative space, emptiness, and vacuity are often the predators of clarity, accuracy, and honesty.

A check is only valuable if it can fail.

Rigor starts light
Rigor follows the risk, up and down
We orbit to achieve understanding

8 of 30 · Background

The idea held; the machinery changed

Ty, the author, reached this process in 2026 by trying a lot of tools, on two machines. The process on top kept changing. The two lanes underneath 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, and which tool.

9 of 30 · Background

Five chapters

2 Apr

The orbital plugins

A Prolog plugin that grows into a seven-stage pipeline with 17 sub-agents. Lesson: ten of ten theorems proven, and the code could still ship broken.

13 Jun

By hand

The pipeline off, lean‑lsp on. Nine Lean commits land in 24 minutes. A refutation pass over a spec's axioms finds a false one.

11 Aug

Raw Claude

One week with no process. Then the formal work comes back, and the hub's new rule is: humans specify, and choose the verification level.

28 Aug

The AIDLC

Ticket #1200 is the first. By 9 September its Lean model has 182 theorems, with no gaps and no axioms.

21 Oct

Sagittarius

Start light. Shift up on a signal. Lean back when it is resolved.

Linux laptop
20 Feb: MacBook Pro
14 Sep: back to Linux, everything copied over

10 of 30 · Background

Three eras, one idea that stayed

Treat the spec as a hypothesis, and try to disprove it before there is code.

1. The orbital plugins

Taught: the tools were strong, but one level of rigor for all work was too strict.

The gap: by hand, then raw Claude

Taught: the old philosophy was sound, but the process had reached a local optimum. Tuning it would not help; it needed a different shape with less machinery.

2. The AIDLC

Taught: a tier chosen once at the start does not work. Nobody knows how much must be formal until a miscommunication happens.

3. Sagittarius

Live: since 21 October 2026, first as Orbital Shifting, a name borrowed from the old pipeline plugin shifting@orbital. Renamed Sagittarius on 22 October, so the two are not confused.

11 of 30 · Background

The AIDLC, renovated twice

The AIDLC tried to scale the process back with tiers. Each renovation aimed to make it lighter; none made the prompt shorter.

13 Oct, the lesson: the tier cannot be chosen once. Start light, and shift up.

12 of 30 · Why

Why the tiers had to go

Tiers had the right philosophy, but they overfit.

Ty wanted three or more tiers. The middle ones emptied, so the gradient was never smooth.

And "difficulty" was the wrong axis. What is hard for a model today is not what will be hard in six months, or in six years.

"I knew it wasn't going to survive the next model shift."

13 of 30 · Why

The constant: misalignment

LLMs scale with data and compute. They don't have the data in your brain.

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, and that will continue to be a point of friction."

So the process aims at the bridge, not at difficulty: find the intent, then deliver it without unnecessary process.

14 of 30 · Why

Two lenses: Lean and Prolog

"Working together, the specificity of Lean and the structure of Prolog help provide two lenses that the LLM and the human can use to determine the intent of the session." (Ty)

Lean: Demands specificity: a statement says exactly what is meant, or it does not check. LLMs use it more and more. In the orbit, it proves the claims that burn.
Prolog: A queryable, self-contained store of facts, with logical constraints that keep the LLM and the human on what matters most. In the orbit, it is the KB.

15 of 30 · The tool

What Sagittarius is

A system prompt, a command-line tool, and two tools it calls: Prolog and Lean. That's all.

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

"My bet is that this version will stand the test of time and continue being used even if harnesses evolve in other ways."

Plain text and a shell command: no harness owns it. Prolog and Lean are older, and steadier, than any agent.

Get the tools: SWI-Prolog · Lean · elan · sharlean · lean-lsp-mcp

16 of 30 · 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. When the work shifts up, the agent runs it.

Each step in full

Install once. SWI-Prolog, and orbit-kb on your PATH. Lean 4 only if you want proofs. Then run orbit-kb doctor.
Load the prompt. Append SAGITTARIUS.md to the agent's system prompt. For Claude Code, run claude --append-system-prompt "$(cat ~/.claude/sagittarius/SAGITTARIUS.md)". A shell function or alias makes this the default for every session.
Ask in your own words. A question gets an answer. A change starts on the light path. A report of a problem starts discovery.
Answer what it asks. At most three questions a round, each with options and a marked default.
Verify the result, not the tests. The delivery says what was checked, what was guessed, and what was not checked.

What the agent runs

$ orbit-kb init kb --request 'Make the button purple' --uses build
$ orbit-kb add "claim(c1, introduce, 'Primary buttons are purple.')" "check(k1, c1)"
$ orbit-kb run k1 -- npm test -- button     # fails first, then passes
$ orbit-kb query done                       # exit 0 means yes
$ orbit-kb report                           # the delivery skeleton

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.

17 of 30 · How it works

Parallax: one lap of the orbit

Each party sees the intent from a different position. Like two eyes, the views triangulate the intent. Where they do not line up, there is a divergence.

Each lap passes through the formal artifacts and through the human, so no one party grades its own work. Most tickets close in one lap.

18 of 30 · How it works

Two orbits: discovery, then build

When discovery runs, it comes first. A clear request skips it.

We write solutions to problems. We do not write to achieve understanding; we orbit to achieve understanding.

19 of 30 · How it works

Where a request goes

A report says something is wrong or wanted, but not what to change. A change request with open details stays in the build orbit: open details are questions to ask, not a reason for discovery.

20 of 30 · How it works

The light path

Most tickets need only these five steps. They are the whole process until a trigger fires.

Get it right, not get it done.

One try to get the request right; the human's verification closes it. A result that only looks done hides a divergence, so the agent reports what it did not verify.

The steps in full

State the request back in a sentence, with one concrete example.
Decide: ask first, or build on assumptions. Ask first only if a wrong default is costly or impossible to undo (data loss, external effects, public interfaces, security, money), or two defaults are equally likely and the build is large. At most three questions in one round, with options and a marked default.
Write the check first, and run it. A check of behavior that the change adds or removes must fail before the change. A check that current behavior stays the same passes before and after. If there is no executable check, say so under "Not checked".
Build only what the request needs.
Run the checks again. Deliver with the report, and say "No KB". The report names each check and its result in one line; it is not a test report for the human to review.

21 of 30 · How it works

Shift up on a signal. Lean back when it is resolved.

Questions

More than three, or an answer raises a new one.

A divergence

That is wrong. Or a check, or the code, surprises the agent.

A claim burns

It needs a proof (slide 25).

A handoff

Another session continues the work.

When the agent leans back, it says so in one line: Leaning back: <what stopped>. Still active: <what continues>.

Why not start with a KB?

A KB costs time, so the agent does not start one before it needs one. A KB is memory and a referee, so the agent starts one as soon as a miscommunication or a proof appears. On a shift up, it records the request, the claims, the checks, and the answers so far, and continues in the KB.

22 of 30 · How it works

The build orbit, in a KB

After a shift up, the agent works in the KB with moves. It runs only the moves the ticket needs, and every move reads the ticket text itself.

done = nothing under, over, or to ask; no burn open
Only orbit-kb writes the KB

The moves in full

SURVEY: record the current behavior that the claims depend on. For a defect, reproduce it first. Skip it when discovery ran, or when the change site is obvious.
DECOMPOSE: split the ticket into claims: preserve, retire, or introduce. Each cites the ticket text and has concrete examples. Questions stay dormant, with defaults.
BUILD: write the checks first, plus a screenshot check for a user surface. Run each retire and introduce check red. Never edit a check to make it pass.
FULFILL: review with fresh eyes, both ways. Under: a claim not fulfilled. Over: a change that serves no claim.
DISPROVE: try to break a claim on a small budget. The verdict is refuted(Counterexample), inconclusive, or abstained. Do not weaken a claim to absorb a counterexample.
BURN: prove a burning claim in Lean (slide 25). EXPLAIN: on request.
One logic engine, SWI-Prolog, answers each KB query. not p holds when p has no answer. Exit 2 is never a "no".

23 of 30 · How it works

The discovery orbit

Discovery turns a report into a ticket with a clear problem, scope, and risk, before anything is built. Most reports need only a reproduction.

Tiny one problem, a cheap reproduction
Full, in a KB on a trigger, or when a claim needs a model

The full discovery orbit

Pin the report as one falsifiable hypothesis, then touch the system to reproduce it. If it does not reproduce, tell the human what was tried. Three laps by default.
Choose the cheapest tool that can falsify each claim: a reproduction or a test first; SMT (a solver for rules, permissions, limits, prices); TLA+ (a model checker for order of steps, retries, concurrency). A property for every input is universal, for BURN.
A finding from a model only is a lead, until a reproduction on the system confirms it.
Ask only the questions that evidence raised: conflicts first, then surprises, then boundaries. When stakeholders conflict, the decision owner decides.
Stop when discovery is ready, or the budget is spent. Out of budget is not ready: report what is known and not known. Then vote.
A wrong report is a valid result. Say so, with the evidence.

Moves: SIGNAL, SURVEY, SPECTRUM, FLYBY (SMT), TRAJECTORY (TLA+), DISPROVE.

24 of 30 · How it works

The vote: GO, NO-GO, or HOLD

At the end of discovery, three roles vote. A choice wins with more than 0.5 of the vote. No role wins alone, and nothing wins without the human.

A split is recorded as a divergence, and another orbit follows.

GO build the ticket
NO-GO not real, already exists, or not worth it
HOLD wait for data, access, or a decision; then lap again

Who votes how

The agent votes first, sealed

Recorded before the report. A visible vote biases the human.

The artifacts vote by rule

In a KB, the tool computes it. In a tiny orbit: red reproduction is GO; no reproduction is NO-GO.

The human decides

Nothing is built or dropped against the human's vote.

25 of 30 · How it works

Burns: when a test cannot be enough

A claim burns when it is universal, when the human asks for a proof, or when it was contested twice. Universal has one meaning: the domain inputs are infinite or too large to check case by case.

Burns "No discount code takes a price below the floor."
Does not burn "Primary buttons are purple." A few examples cover it.

The rules and the steps

A statement with sorry is not a proof. "No counterexample in N trials" is not a proof. A solver result or a TLC run holds only within its encoding and bounds.
If a Lean file or a Lake configuration file changes, the proof stops counting. A claim that supersedes a burning claim needs its own proof.
A proof shows the theorem holds for the Lean model. It does not show the shipped code matches the model (only checks test the code), or that the statement says what the claim says (the human reads that).
If the proof fails, the claim or the model is wrong, or not yet clear. That is a divergence: record it and ask. Do not weaken the claim to fit the proof.

Write a Lean model of the behavior, and state the claim as a theorem.
Add #eval examples, and show them to the human as a table.
Search for a counterexample first. If one turns up, record refuted(Counterexample) and ask the human.
Prove it, and record it with orbit-kb prove. Read back the printed statement and show it to the human.
Carry each Lean example back to the code as a test case.

Waivers. Only a human can skip work. A skip is a waiver with a due time; it can target a burn, a check, or a question. A waived check covers its claim (not unfinished, but not fulfilled either, and the delivery says so). After the due time, the item blocks done again.

26 of 30 · How it works

Trust and honesty

The formal artifacts catch honest mistakes. They do not stop cheating, and the prompt says so.

Known limits

orbit-kb cannot verify --by human. orbit-kb prove does not resist a proof built to fool it.

So the agent

records --by human only for what the human said, and never works around a check. A safeguard that is worked around protects no one.

Match the words to the evidence

Evidence	Not	Say
Tests pass	"correct"	"the checks pass"
Stated in Lean	"proved"	"stated, not proved"
Proved in Lean	"the code is proved"	"proved for the model"
No counterexample in 1,000 trials	"always true"	"none found in 1,000 trials"

Three more honesty rules

Every default is a guess: list the risky ones
Disclosing is never a failure; hiding is
Found your own work wrong? Say so first

27 of 30 · How it works

The delivery

Six fields, in short plain sentences. An empty field says "none", so the human sees that the agent looked. An example from the light path:

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.

With a KB

orbit-kb report drafts it and adds Open:: open burns, lapsed waivers, proofs that no longer count.

Waivers

Every waiver is listed, with its due time.

Screenshots

When the change has a user surface.

Landing

The agent lands the change when it judges it safe, within the harness guardrails. It stops for the human first when the change touches a public interface, data, security, or money, or is hard to undo. Then "To land" names the decision.

28 of 30 · The gradient

The lightest path

The five steps of slide 20, on one real ticket. No KB.

Most tickets end here: red, then green, then the human says yes.

What would shift it up

The human says that is not what I meant: a divergence. Or asks that every button keep 7:1 contrast: a claim that burns. Then a KB starts: the gradient.

29 of 30 · The gradient

The most rigorous path

The report: Some stacked discount codes give orders for almost nothing.

The claim: no discount code takes a price below the floor (the lowest price allowed).

Rigor that can guarantee the claim, for the Lean model.

Many laps, two orbits
Hours, not minutes
Only when a signal demands it: here, a universal claim

Every station, in order

SIGNAL, SURVEY. The report becomes one hypothesis, a defect, with a budget of three laps. The agent reproduces it on the system: a red test.
FLYBY. An SMT model of the existing rules makes the stacked-code case SAT. The target rules make it UNSAT, within the encoding and its bounds.
TRAJECTORY. A TLA+ model of apply, remove, and retry, with the rules as guards. A trace raises a question for the human.
Laps. Each lap touches the system or a solver, then the human. An answer that changes a claim supersedes it, and another lap follows.
DISPROVE. A fresh subagent attacks the claims. Each counterexample is recorded and becomes a test case.
Vote. The agent votes first, sealed. The artifacts vote by rule. The human reads the report and votes. GO needs more than 0.5, so it needs the human.
Build. Same KB. Claims labeled preserve, retire, or introduce; questions stay dormant with defaults. Checks are written first, and fail before they pass.
BURN. The claim is universal. A Lean model, #eval examples as a table for the human, and a counterexample search first. Then the proof, recorded by orbit-kb prove. The human reads the printed statement.
Delivery. done holds: nothing under, over, or to ask, and no open burn. Each Lean example is a test. Prices are money, so the human decides to land.

30 of 30 · The gradient

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.

"My bet is that this version will stand the test of time and continue being used even if harnesses evolve in other ways. This pattern offers, when it really needs it, a level of rigor that can guarantee correctness."

What "guarantee" covers: a proof holds for every case of the Lean model. The checks tie the model to the code.

Sources: the live prompt, prompt/SAGITTARIUS.md (live since 2026-10-21), its design notes thoughts/orbital-shifting-system-prompt-draft.md, and thoughts/orbital-shifting-refinement-record.md. Slides 8 to 11 come from thoughts/orbital-shifting-history.md. Slides 12 to 14 quote thoughts/orbital-shifting-why.md. The thoughts/ files are in git history, at the tag thoughts-archive.

Without JavaScript, scroll.