AI agents · Formal verification · Developer tools

Invariant

You decide what must be true. It proves the code.

A code factory that turns GitHub issues into merged pull requests, with code proved against statements a person ratified on the issue.

Issue #1, from opened to merged

The factory’s first real issue, replayed from what GitHub recorded, in UTC on September 25, 2026. Open any step to read what was said.

17:58:4418:25:00

Invariant reads the issue and asks 42s
Joseph decides 3m 28s
Invariant proposes and checks with TLC 1m 15s
Joseph reviews and ratifies 6m 50s
Invariant writes and proves the code 2m 5s
CI’s gate, then the merge 11m 56s

17:58:44 +0sJoseph opened issue #1Add a bounded buffer for log shipping
“Add a bounded buffer for log shipping”, opened by Joseph as @gitdek.
17:59:26 +42sInvariant asked two questions instead of guessing42 seconds after the issue opened
◉ Invariant 17:59:26
Before I write down what must be true for this issue, I need you to decide:
F1. When a producer writes a line and the buffer is already at capacity, what should happen?
- A. The producer waits until the shipper frees a slot, so no line is ever lost. Joseph’s choice
- B. The new line is dropped and the producer carries on, so the buffer keeps the older lines.
- C. The oldest line in the buffer is discarded to make room for the new one, so the buffer keeps the newest lines.
- D. The write is refused with an error returned to the producer, which decides what to do next.
F2. When the shipper fails to send a line, what should happen to that line?
- A. The line stays at the front of the buffer and the shipper retries it before sending any later line. Joseph’s choice
- B. The line is dropped and the shipper moves on to the next line.
18:02:54 +4m 10sJoseph decidedF1 A and F2 A
Joseph 18:02:54
```
/invariant choose F1 A
/invariant choose F2 A
```
- F1 A. The producer waits until the shipper frees a slot, so no line is ever lost.
- F2 A. The line stays at the front of the buffer and the shipper retries it before sending any later line.
18:04:09 +5m 25sInvariant proposed 13 statements6 invariants, 3 witnesses and 3 known bugs, already checked by TLC
◉ Invariant 18:04:09
Here's what I propose must always be true for bounded log shipping buffer. Once you ratify it, these statements are pinned by hash, and I can't change them.
The spec
- Spec The system starts in Init, and every step is a Next step.
Invariants: what must never go wrong
- TypeOK The buffer, the shipped lines and the write history are lists of log lines, each producer has written a bounded number of lines, and the shipper is either retrying or not.
- BoundedCapacity The buffer never holds more lines than its capacity.
- NoLineLost Every line a producer has written is either still in the buffer or has been shipped.
- ShippedOnce No line is shipped more than once.
- ShippedInOrder The shipped lines are exactly the oldest written lines, in the order they were written.
- BufferInOrder The buffer holds exactly the written lines not yet shipped, oldest first.
Witnesses: outcomes that must be reachable
- BufferFull The buffer can fill up to its capacity.
- RetryPending A send can fail and leave its line in the buffer to be retried.
- AllShipped Every producer can finish writing and every line can be shipped.
Known bugs: mistakes the invariants must catch
- WriteOverCapacity A producer adds a line to a buffer that is already full. It must break BoundedCapacity.
- DropOnFailure When a send fails, the line is thrown away instead of retried. It must break NoLineLost.
- ResendDelivered A send that actually went through is treated as failed and retried, so the line is shipped twice. It must break ShippedOnce.
Already checked against a draft model, within Capacity = 2, MaxLines = 2, Producers = {p1, p2}: TLC explored 87 states and found no violation and no deadlock, all 3 witnesses were reached, and the known bugs WriteOverCapacity, DropOnFailure, ResendDelivered were caught.
The statements in TLA+
```
vars == <<buf, sent, log, written, retrying>>

Lines == Producers \X (1..MaxLines)

Range(s) == {s[i] : i \in DOMAIN s}

TypeOK ==
    /\ buf \in Seq(Lines)
    /\ sent \in Seq(Lines)
    /\ log \in Seq(Lines)
    /\ written \in [Producers -> 0..MaxLines]
    /\ retrying \in BOOLEAN

BoundedCapacity == Len(buf) <= Capacity

NoLineLost == \A i \in 1..Len(log) : log[i] \in Range(sent) \cup Range(buf)

ShippedOnce == \A i, j \in 1..Len(sent) : i # j => sent[i] # sent[j]

ShippedInOrder ==
    /\ Len(sent) <= Len(log)
    /\ sent = SubSeq(log, 1, Len(sent))

BufferInOrder ==
    /\ Len(sent) <= Len(log)
    /\ buf = SubSeq(log, Len(sent) + 1, Len(log))

BufferFull == Len(buf) = Capacity

RetryPending == retrying /\ buf # <<>>

AllShipped ==
    /\ \A p \in Producers : written[p] = MaxLines
    /\ buf = <<>>
    /\ Len(sent) = Len(log)
    /\ Len(log) > 0

WriteOverCapacity ==
    \E p \in Producers :
        /\ written[p] < MaxLines
        /\ Len(buf) = Capacity
        /\ LET line == <<p, written[p] + 1>> IN
            /\ buf' = Append(buf, line)
            /\ log' = Append(log, line)
        /\ written' = [written EXCEPT ![p] = @ + 1]
        /\ UNCHANGED <<sent, retrying>>

DropOnFailure ==
    /\ buf # <<>>
    /\ buf' = Tail(buf)
    /\ retrying' = FALSE
    /\ UNCHANGED <<sent, log, written>>

ResendDelivered ==
    /\ buf # <<>>
    /\ sent' = sent \o <<Head(buf), Head(buf)>>
    /\ buf' = Tail(buf)
    /\ retrying' = FALSE
    /\ UNCHANGED <<log, written>>

Spec == Init /\ [][Next]_vars
```
18:10:59 +12m 15sJoseph ratifiedproposal e5dca8da9f15
Joseph 18:10:59
```
/invariant ratify e5dca8da9f15
```
◉ Invariant 18:11:18
Ratified by @gitdek. I pinned 13 statements in examples/03-log-buffer on branch invariant/issue-1-log-buffer (proposal sha256:e5dca8da9f15). Writing the code now.
From here the 13 statements are pinned by hash. The factory can’t change them, and CI checks that a person with write access ratified exactly this proposal.
18:13:04 +14m 20sInvariant opened #2: provedGobra: 5 of 5 functions · the code reaches all 87 states
◉ Invariant 18:13:06
The code is written, and it passed the gate here: it's proved. I opened #2, and I'll merge it once CI's invariant/gate passes on it.
An AI coding agent wrote the code in 8 turns, confined to its workspace, and the gate passed on run 1 of 1.
The receipt
18:25:00 +26m 16sInvariant merged #2 once CI’s gate passedas 3ce3ba3
◉ Invariant 18:25:03
CI's invariant/gate passed on #2, and I merged it as 3ce3ba3a5ca07acd2bb422902c945fb43a80de59.
The pull request closed issue #1 at 18:25:02.

People decide, the factory proves

AI coding agents don’t ask clarifying questions. They pick an interpretation and ship it confidently. A proof alone doesn’t fix that: if the agent also wrote the property, the proof only certifies the agent’s guess.

Invariant splits the work. People decide what must be true, on the issue, and the factory proves that the code satisfies it.

Formalize. An agent reads the issue and drafts formal statements in TLA+: invariants, what must never go wrong; witnesses, outcomes that must be reachable; and known bugs, plausible mistakes the invariants must catch.
Ask. When the issue allows materially different behaviors, the factory doesn’t pick. It posts the question on the issue and waits.
Ratify. The factory checks its draft with the TLC model checker before anyone sees it. A person with write access ratifies it with a comment, and the statements are pinned by hash.
Synthesize. An agent writes the code against the ratified statements, confined to its workspace. The gate checks it, and the agent gets up to three repairs.
Gate and merge. CI re-runs every check. The factory merges its own pull request only when the gate passes on that exact commit.

One contract per action

Each Go function carries a Gobra contract that restates exactly one TLA+ action. The action’s enabling condition becomes the contract’s precondition, and its effect, including everything it leaves unchanged, becomes the postconditions.

In two-phase commit, Gobra verified all 10 functions against their contracts, with integer overflow checked, and the Go code reaches exactly the model’s 288 states. Choose a clause to see its match.

RMPrepare, in TLA+ and in Go

TLA+ · TwoPhase.tla, lines 72 to 76

72RMPrepare(r) ==73    /\ rmState[r] = "working"74    /\ rmState' = [rmState EXCEPT ![r] = "prepared"]75    /\ msgs' = msgs \cup {[type |-> "Prepared", rm |-> r]}76    /\ UNCHANGED <<tmState, tmPrepared>>

Go with its Gobra contract · twophase.go, lines 96 to 109

96// RMPrepare mirrors RMPrepare(r): a working resource manager prepares and97// tells the transaction manager.98// @ requires 0 <= r && r < N99// @ requires s.RM[r] == Working100// @ ensures t.RM[r] == Prepared && t.PreparedMsg[r]101// @ ensures forall i int :: 0 <= i && i < N && i != r ==> t.RM[i] == s.RM[i] && t.PreparedMsg[i] == s.PreparedMsg[i]102// @ ensures t.TM == s.TM && t.TMPrepared == s.TMPrepared103// @ ensures t.CommitMsg == s.CommitMsg && t.AbortMsg == s.AbortMsg104func RMPrepare(s State, r int) (t State) {105	t = s106	t.RM[r] = Prepared107	t.PreparedMsg[r] = true108	return t109}

Choose a clause, in either language, to see its match.

The action takes one resource manager, r. The contract requires r to be one of the resource managers.

The action can only happen while r is working. The TLA+ guard is the contract’s requires.

r becomes prepared and its Prepared message goes out. The effect is the first ensures.

UNCHANGED keeps the coordinator’s state and its recorded votes. The frame lines in the contract also spell out what EXCEPT and the set union leave alone: the other resource managers and messages.

go run ./cmd/invariant verify -out out/02-twophase-commit examples/02-twophase-commit

Pinned statements ✓ 6 of 6 match · recorded in D-0027

Design · TLC ✓ no violations, no deadlock · 288 distinct states (1,146 generated), depth 11

Reachability ✓ 2 of 2 witnesses reached · AllCommitted in 10 steps, AllAborted in 3 steps

Known bugs ✓ 1 of 1 caught · early-commit: TCConsistent violated after 5 steps

Agreement ✓ code reaches the model's states · 288 states, depth 11

Code · Gobra ✓ proved: 10 of 10 functions verified · 10 with contracts, overflow checked, not verified: Successors

Build ✓ go vet, go test · sandboxed, no network

Checked within RM = {r1, r2, r3}. Within these bounds TLC’s search is exhaustive. Nothing is claimed outside them.

✓ Pass. Every check passed. The code is proved. Fingerprint sha256:2a0189e69e1f

The receipt on the pull request

The factory opened #2 once the code passed the gate on Joseph’s machine, and merged it only after CI’s invariant/gate passed on that exact commit.

In CI, the gate also checks that a factory pull request touches only its own project, and confirms on GitHub that a person with write access ratified exactly the proposal in the lock.

Merged Add a bounded buffer for log shipping #2

invariant/gate · proved · 87 states, exhaustive within bounds · merged by the factory Receipt

◉ Invariant receipt · bounded log shipping buffer

✓ Pass. Every check passed. The code is proved.

Check	Result	Evidence
Pinned statements	✓ 13 of 13 match	ratified by @gitdek on #1 at 18:10:59
Design · TLC	✓ no violations, no deadlock	87 distinct states (159 generated), depth 9
Reachability	✓ 3 of 3 witnesses reached	`BufferFull` in 2 steps, `RetryPending` in 2 steps, `AllShipped` in 8 steps
Known bugs	✓ 3 of 3 caught	write-over-capacity: `BoundedCapacity` violated after 3 steps; drop-on-failure: `NoLineLost` violated after 2 steps; resend-delivered: `ShippedOnce` violated after 2 steps
Agreement	✓ code reaches the model’s states	87 states, depth 9
Code · Gobra	✓ proved: 5 of 5 functions verified	5 with contracts, overflow checked, not verified: Successors
Build	✓ go vet, go test	sandboxed, no network · `go test` found no test files

Checked within Capacity = 2, MaxLines = 2, Producers = {p1, p2}. Within these bounds TLC’s search is exhaustive. Nothing is claimed outside them.

Fingerprint sha256:dfaf31c67a3f78c8909ce205f89823204aa20237a2b2b69553cba0817064d31f

The same fingerprint came from the run that opened #2, at 18:13:02, and from a later re-run at 18:46:09.

What it doesn’t do yet

Invariant checks safety, not liveness: that nothing bad happens, not that something good eventually does. Model checking is exhaustive only within the bounds each receipt states, and nothing is claimed outside them.

The log buffer’s model assumes the shipper knows whether a send succeeded. The factory builds new projects only, and writes Go only. Existing TypeScript and Python code can be tested against a model instead of proved, and a receipt always says which kind of evidence it carries.

Current status

Invariant runs on Joseph’s machine: invariant watch polls GitHub through the gh command-line tool and hands the writing to AI coding agents. Invariant itself is written in Go.

The repository is private for now, so issue #1 and pull request #2 are named here without links.

Invariant

Issue #1, from opened to merged

F1. When a producer writes a line and the buffer is already at capacity, what should happen?

F2. When the shipper fails to send a line, what should happen to that line?

The spec

Invariants: what must never go wrong

Witnesses: outcomes that must be reachable

Known bugs: mistakes the invariants must catch

People decide, the factory proves

A planted bug, caught

One contract per action

The receipt on the pull request

What it doesn’t do yet

Current status

More work

Have somethingin mind?