Available for consulting

All work

AI agents · Formal verification · Developer tools

Invariant

You decide what must be true. The factory checks the code against it.

A code factory that turns GitHub issues into merged pull requests. The code is checked against statements a person ratified on the issue: proved with Gobra or Nagini, or tested against the model, and every receipt says which.

Watch it live

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.

  • 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
  1. +0sJoseph opened issue #1Add a bounded buffer for log shipping

    “Add a bounded buffer for log shipping”, opened by Joseph as @gitdek.

  2. +42sInvariant asked two questions instead of guessing42 seconds after the issue opened

    ◉ Invariant

    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.
  3. +4m 10sJoseph decidedF1 A and F2 A

    Joseph 

    /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.
  4. +5m 25sInvariant proposed 13 statements6 invariants, 3 witnesses and 3 known bugs, already checked by TLC

    ◉ Invariant

    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
  5. +12m 15sJoseph ratifiedproposal e5dca8da9f15

    Joseph 

    /invariant ratify e5dca8da9f15

    ◉ Invariant

    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.

  6. +14m 20sInvariant opened #2: provedGobra: 5 of 5 functions · the code reaches all 87 states

    ◉ Invariant

    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

  7. +26m 16sInvariant merged #2 once CI’s gate passedas 3ce3ba3

    ◉ Invariant

    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 checks

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 checks the code against it: proved with Gobra in Go or Nagini in Python, or tested against the model in TypeScript and Python. Every receipt says which.

  1. 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.
  2. Ask. When the issue allows materially different behaviors, the factory doesn’t pick. It posts the question on the issue and waits.
  3. 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.
  4. Synthesize. An agent writes the code in Go, TypeScript or Python against the ratified statements, confined to its workspace. The gate checks it, and the agent gets up to three repairs.
  5. 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 morning, 17 pull requests

On Sunday, September 27, from 7 AM to noon Eastern, 17 pull requests merged into Invariant. Three of them went from a plain-language issue to a merge on their own, written and merged by the factory’s bot: a connection pool proved at every size, the factory’s own crash recovery, and a rate limiter with its model bounds taken out of the code. The rest changed Invariant itself: its gate, its watcher and its dashboard.

“Proved at every size” is new that morning. The code carries no model bounds, and Gobra proves it against its contracts at every size. The design’s rules are claimed only within the sizes TLC checked: the bounds a person ratified, and one size past them.

A timeline of the morning: three issues the factory took from plain language to a merge, above the fourteen pull requests that changed Invariant itself
From GitHub’s own timestamps. Each merge passed CI’s gate first.

  1. #18 to #20 20 minutes of factory time, CI included, and 1 comment from a person

    Merged A connection pool that never hands out more than it has #20

    invariant/gate · proved at every size · 13 states, and 73 one size larger · merged by the factory Receipt

    ✓ Pass. Every check passed. The code is proved at every size. Fingerprint sha256:b432097d509b

    CheckResultEvidence
    Pinned statements✓ 9 of 9 matchratified by @gitdek on #18
    Design · TLC✓ no violations, no deadlock13 distinct states (55 generated), depth 3
    Reachability✓ 2 of 2 witnesses reachedPoolFull in 2 steps, SomeoneHolds in 1 step
    Known bugs✓ 2 of 2 caughtacquire-when-full: NeverOverSize violated after 3 steps, acquire-twice: AtMostOnePerClient violated after 2 steps
    Agreement✓ code reaches the model's states13 states, depth 3
    One size larger✓ code reaches the model's states73 states, depth 4, within Clients = {c1, c2, c3, c4}, Size = 3
    Code · Gobra✓ proved: 3 of 3 functions verified3 with contracts, overflow checked, not verified: Init, load, store, Successors
    Build✓ go vet, go testsandboxed, no network

    Checked within Clients = {c1, c2, c3}, Size = 2, and again one size larger, within Clients = {c1, c2, c3, c4}, Size = 3. Within each, TLC's search is exhaustive. Gobra proves the code against its contracts at every size, and the design's rules are claimed only within the sizes checked.

    An AI coding agent wrote the code in 9 turns, and the gate passed on run 2.

  2. #23 to #25 31 minutes of factory time, CI included, and 1 comment from a person

    Merged Prove the factory recovers from a crash at any point, and from a second watcher #25

    invariant/gate · proved at every size · 5,188 states, and 39,550 one size larger · merged by the factory Receipt

    ✓ Pass. Every check passed. The code is proved at every size. Fingerprint sha256:01e74cf660f9

    CheckResultEvidence
    Pinned statements✓ 23 of 23 matchratified by @gitdek on #23
    Design · TLC✓ no violations, no deadlock5,188 distinct states (16,312 generated), depth 28
    Reachability✓ 5 of 5 witnesses reachedMerged in 15 steps, ReportedUnmergeable in 14 steps, StoppedRunReported in 12 steps, RetryBuilt in 18 steps, RecoveredAfterCrashes in 17 steps
    Liveness · TLC✓ 2 of 2 properties holdCommandsAnswered holds, GatedPullRequestsSettled holds, under FairAcquire, FairExpire, FairAct, FairFinishRun, FairDropRun
    Fairness✓ 5 of 5 on steps the model takesFairAcquire: weak, on Acquire(w), FairExpire: weak, on Expire, FairAct: weak, on Act(w), FairFinishRun: weak, on FinishRun(w), FairDropRun: weak, on DropRun(w)
    Known bugs✓ 3 of 3 caughtpost-without-looking: NoDoubleAnswer violated after 4 steps, post-without-lease: OnlyHolderActs violated after 2 steps, rerun-stopped-run: NoRunTwice violated after 6 steps
    Agreement✓ code reaches the model's states5,188 states, depth 28
    One size larger✓ code reaches the model's states39,550 states, depth 30, within MaxCrashes = 3, Watchers = {w1, w2, w3}
    Code · Gobra✓ proved: 31 of 31 functions verified31 with contracts, overflow checked, not verified: b2i, runIndex, repoOf, withRepo, watcherOf, Init, Successors
    Build✓ go vet, go testsandboxed, no network

    Checked within MaxCrashes = 2, Watchers = {w1, w2}, and again one size larger, within MaxCrashes = 3, Watchers = {w1, w2, w3}. Within each, TLC's search is exhaustive. Gobra proves the code against its contracts at every size, and the design's rules are claimed only within the sizes checked.

    An AI coding agent wrote the code in 8 turns, and the gate passed on run 1.

  3. #28 to #30 42 minutes of factory time, CI included, and 1 comment from a person

    Merged Take the rate limiter's model bounds out of its code #30

    invariant/gate · tested against the model · 19,489 states · merged by the factory Receipt

    ✓ Pass. Every check passed. The code is tested against the model. Fingerprint sha256:2e143ead1b0f

    CheckResultEvidence
    Pinned statements✓ 17 of 17 matchratified by @gitdek on #28, amending #5
    Design · TLC✓ no violations, no deadlock19,489 distinct states (29,000 generated), depth 14
    Reachability✓ 5 of 5 witnesses reachedBurstGoesOut in 2 steps, CallWaits in 3 steps, WaitingCallGoesOut in 4 steps, BucketRefills in 2 steps, CallRefused in 5 steps
    Known bugs✓ 4 of 4 caughtsend-without-token: WithinRate violated after 3 steps, jump-queue: FirstInFirstOut violated after 5 steps, queue-past-limit: BoundedWait violated after 5 steps, refuse-early: NoNeedlessRefusal violated after 3 steps
    One size larger not claimedTLC didn't finish one size larger within 3m0s: context deadline exceeded
    Code · conformance✓ tested against the model: every reachable state, no step outside it28999 runs, 322,028 steps, 19489 of 19,489 model states visited
    Build✓ node --testsandboxed, no network

    Checked within Apis = {a1, a2}, Capacity = 2, MaxCalls = 5, MaxTime = 3, MaxWaiting = 2. Within these bounds TLC's search is exhaustive. Nothing is claimed outside them.

    An AI coding agent wrote the code in 9 turns, and the gate passed on run 1.

It proved its own crash recovery

The factory’s watcher takes each step on an issue as a few effects on GitHub, and a crash can come between any two of them. Issue #23 asked the factory to model how it recovers, with a second watcher running at the same time, and to prove the core it would run on.

It proposed 23 statements: the spec, 7 invariants, such as no effect ever happening twice; 5 witnesses; 2 liveness properties, such as every command eventually being answered, under 5 fairness assumptions a person ratifies; and 3 known bugs. TLC checked them before anyone saw them, and one comment ratified them.

The factory wrote factory/recovery in Go, and the gate passed on run 1. Gobra proves 31 of 31 functions at every size, and the code agrees with TLC at 5,188 states, and at 39,550 one size larger.

Then the watcher started running on it. It holds a lease in a Git ref, so only one watcher acts at a time, and it records each agent run and merge before it happens. A test stops it just before each of its 20 effects, then restarts it on the same machine or another: all 40 stops recover, with every effect done once. Before the change, stopping before 8 of its 15 effects broke the flow, 14 of 30 stops.

Issue #23 as Joseph wrote it: the watcher’s steps and effects, what a watcher sees, the rules, and what must be true
Issue #23, in plain language. The receipt is with #25 above.
A grid of the crash test: the watcher stopped before each of its 20 effects on the same machine and on another, with every stop now recovering
The crash test, from its real output: 40 stops, 40 recoveries.

A planted bug, caught

A model can pass its checks because nothing ever happens in it. So every proposal also carries witnesses, outcomes that must be reachable, and known bugs: plausible mistakes planted in the model, each of which TLC must catch. That’s how you know the invariants have teeth.

These are the real counterexamples TLC found. Step through the early-commit bug in two-phase commit: 6 states, from every resource manager working to a violation of TCConsistent.

TLC counterexamples

Trace

Planted bug EarlyCommit The coordinator commits once any resource manager has prepared, instead of waiting for all of them.

Steps of the two-phase commit trace

  1. Step 1 of 6

    All three resource managers are working, and the coordinator hasn’t decided.

    Coordinator tmState
    init
    Resource managers rmState
    r1 workingr2 workingr3 working
    Messages msgs
    none
    Votes recorded tmPrepared
    none
    msgs = {}
rmState = (r1 :> "working" @@ r2 :> "working" @@ r3 :> "working")
tmPrepared = {}
tmState = "init"

  2. Step 2 of 6 · RMPrepare

    r1 prepares, and its Prepared message goes out.

    Coordinator tmState
    init
    Resource managers rmState changed
    r1 preparedr2 workingr3 working
    Messages msgs changed
    Prepared r1
    Votes recorded tmPrepared
    none
    msgs = {[type |-> "Prepared", rm |-> r1]}
rmState = (r1 :> "prepared" @@ r2 :> "working" @@ r3 :> "working")
tmPrepared = {}
tmState = "init"

  3. Step 3 of 6 · TMRcvPrepared

    The coordinator records r1’s vote.

    Coordinator tmState
    init
    Resource managers rmState
    r1 preparedr2 workingr3 working
    Messages msgs
    Prepared r1
    Votes recorded tmPrepared changed
    r1
    msgs = {[type |-> "Prepared", rm |-> r1]}
rmState = (r1 :> "prepared" @@ r2 :> "working" @@ r3 :> "working")
tmPrepared = {r1}
tmState = "init"

  4. Step 4 of 6 · RMChooseToAbort

    r2 aborts on its own.

    Coordinator tmState
    init
    Resource managers rmState changed
    r1 preparedr2 abortedr3 working
    Messages msgs
    Prepared r1
    Votes recorded tmPrepared
    r1
    msgs = {[type |-> "Prepared", rm |-> r1]}
rmState = (r1 :> "prepared" @@ r2 :> "aborted" @@ r3 :> "working")
tmPrepared = {r1}
tmState = "init"

  5. Step 5 of 6 · EarlyCommit

    The buggy coordinator commits on r1’s vote alone.

    Coordinator tmState changed
    done
    Resource managers rmState
    r1 preparedr2 abortedr3 working
    Messages msgs changed
    CommitPrepared r1
    Votes recorded tmPrepared
    r1
    msgs = {[type |-> "Commit"], [type |-> "Prepared", rm |-> r1]}
rmState = (r1 :> "prepared" @@ r2 :> "aborted" @@ r3 :> "working")
tmPrepared = {r1}
tmState = "done"

  6. Step 6 of 6 · RMRcvCommitMsg

    r1 receives the Commit message and commits.

    Coordinator tmState
    done
    Resource managers rmState changed
    r1 committedr2 abortedr3 working
    Messages msgs
    CommitPrepared r1
    Votes recorded tmPrepared
    r1
    msgs = {[type |-> "Commit"], [type |-> "Prepared", rm |-> r1]}
rmState = (r1 :> "committed" @@ r2 :> "aborted" @@ r3 :> "working")
tmPrepared = {r1}
tmState = "done"

    TCConsistent violated: r1 has committed while r2 has aborted. The invariant says: No resource manager commits while another aborts.

Planted bug WriteOverCapacity A producer adds a line to a buffer that is already full.

Steps of the log buffer: write over capacity trace

  1. Step 1 of 4

    The buffer is empty.

    Buffer buf
    emptycapacity 2
    Written log
    none
    Shipped sent
    none
    Lines per producer written
    p1 0p2 0
    Retrying retrying
    no
    buf = <<>>
log = <<>>
retrying = FALSE
sent = <<>>
written = (p1 :> 0 @@ p2 :> 0)

  2. Step 2 of 4 · Write

    p1 writes its first line.

    Buffer buf changed
    p1·1capacity 2
    Written log changed
    p1·1
    Shipped sent
    none
    Lines per producer written changed
    p1 1p2 0
    Retrying retrying
    no
    buf = <<<<p1, 1>>>>
log = <<<<p1, 1>>>>
retrying = FALSE
sent = <<>>
written = (p1 :> 1 @@ p2 :> 0)

  3. Step 3 of 4 · Write

    p1 writes its second line, and the buffer is full.

    Buffer buf changed
    p1·1p1·2capacity 2
    Written log changed
    p1·1p1·2
    Shipped sent
    none
    Lines per producer written changed
    p1 2p2 0
    Retrying retrying
    no
    buf = <<<<p1, 1>>, <<p1, 2>>>>
log = <<<<p1, 1>>, <<p1, 2>>>>
retrying = FALSE
sent = <<>>
written = (p1 :> 2 @@ p2 :> 0)

  4. Step 4 of 4 · WriteOverCapacity

    The buggy producer p2 writes anyway.

    Buffer buf changed
    p1·1p1·2p2·1capacity 2
    Written log changed
    p1·1p1·2p2·1
    Shipped sent
    none
    Lines per producer written changed
    p1 2p2 1
    Retrying retrying
    no
    buf = <<<<p1, 1>>, <<p1, 2>>, <<p2, 1>>>>
log = <<<<p1, 1>>, <<p1, 2>>, <<p2, 1>>>>
retrying = FALSE
sent = <<>>
written = (p1 :> 2 @@ p2 :> 1)

    BoundedCapacity violated: the buffer holds 3 lines, and its capacity is 2. The invariant says: The buffer never holds more lines than its capacity.

Planted bug DropOnFailure When a send fails, the line is thrown away instead of retried.

Steps of the log buffer: drop on failure trace

  1. Step 1 of 3

    The buffer is empty.

    Buffer buf
    emptycapacity 2
    Written log
    none
    Shipped sent
    none
    Lines per producer written
    p1 0p2 0
    Retrying retrying
    no
    buf = <<>>
log = <<>>
retrying = FALSE
sent = <<>>
written = (p1 :> 0 @@ p2 :> 0)

  2. Step 2 of 3 · Write

    p1 writes a line.

    Buffer buf changed
    p1·1capacity 2
    Written log changed
    p1·1
    Shipped sent
    none
    Lines per producer written changed
    p1 1p2 0
    Retrying retrying
    no
    buf = <<<<p1, 1>>>>
log = <<<<p1, 1>>>>
retrying = FALSE
sent = <<>>
written = (p1 :> 1 @@ p2 :> 0)

  3. Step 3 of 3 · DropOnFailure

    A send fails, and the buggy shipper throws the line away.

    Buffer buf changed
    emptycapacity 2
    Written log
    p1·1
    Shipped sent
    none
    Lines per producer written
    p1 1p2 0
    Retrying retrying
    no
    buf = <<>>
log = <<<<p1, 1>>>>
retrying = FALSE
sent = <<>>
written = (p1 :> 1 @@ p2 :> 0)

    NoLineLost violated: line p1·1 was written, but it is neither in the buffer nor shipped. The invariant says: Every line a producer has written is either still in the buffer or has been shipped.

Planted bug ResendDelivered A send that actually went through is treated as failed and retried, so the line is shipped twice.

Steps of the log buffer: resend delivered trace

  1. Step 1 of 3

    The buffer is empty.

    Buffer buf
    emptycapacity 2
    Written log
    none
    Shipped sent
    none
    Lines per producer written
    p1 0p2 0
    Retrying retrying
    no
    buf = <<>>
log = <<>>
retrying = FALSE
sent = <<>>
written = (p1 :> 0 @@ p2 :> 0)

  2. Step 2 of 3 · Write

    p1 writes a line.

    Buffer buf changed
    p1·1capacity 2
    Written log changed
    p1·1
    Shipped sent
    none
    Lines per producer written changed
    p1 1p2 0
    Retrying retrying
    no
    buf = <<<<p1, 1>>>>
log = <<<<p1, 1>>>>
retrying = FALSE
sent = <<>>
written = (p1 :> 1 @@ p2 :> 0)

  3. Step 3 of 3 · ResendDelivered

    The send goes through, but the buggy shipper treats it as failed and sends it again.

    Buffer buf changed
    emptycapacity 2
    Written log
    p1·1
    Shipped sent changed
    p1·1p1·1
    Lines per producer written
    p1 1p2 0
    Retrying retrying
    no
    buf = <<>>
log = <<<<p1, 1>>>>
retrying = FALSE
sent = <<<<p1, 1>>, <<p1, 1>>>>
written = (p1 :> 1 @@ p2 :> 0)

    ShippedOnce violated: line p1·1 was shipped twice. The invariant says: No line is shipped more than once.

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
RMPrepare(r) ==    /\ rmState[r] = "working"    /\ rmState' = [rmState EXCEPT ![r] = "prepared"]    /\ msgs' = msgs \cup {[type |-> "Prepared", rm |-> r]}    /\ UNCHANGED <<tmState, tmPrepared>>
Go with its Gobra contract · twophase.go, lines 96 to 109
// RMPrepare mirrors RMPrepare(r): a working resource manager prepares and// tells the transaction manager.// @ requires 0 <= r && r < N// @ requires s.RM[r] == Working// @ ensures t.RM[r] == Prepared && t.PreparedMsg[r]// @ ensures forall i int :: 0 <= i && i < N && i != r ==> t.RM[i] == s.RM[i] && t.PreparedMsg[i] == s.PreparedMsg[i]// @ ensures t.TM == s.TM && t.TMPrepared == s.TMPrepared// @ ensures t.CommitMsg == s.CommitMsg && t.AbortMsg == s.AbortMsgfunc RMPrepare(s State, r int) (t State) {	t = s	t.RM[r] = Prepared	t.PreparedMsg[r] = true	return t}

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.

CheckResultEvidence
Pinned statements✓ 13 of 13 matchratified by @gitdek on #1 at 18:10:59
Design · TLC✓ no violations, no deadlock87 distinct states (159 generated), depth 9
Reachability✓ 3 of 3 witnesses reachedBufferFull in 2 steps, RetryPending in 2 steps, AllShipped in 8 steps
Known bugs✓ 3 of 3 caughtwrite-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 states87 states, depth 9
Code · Gobra✓ proved: 5 of 5 functions verified5 with contracts, overflow checked, not verified: Successors
Build✓ go vet, go testsandboxed, 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.

Receipts claim only what was checked

Issue #28 asked the factory to take the TypeScript rate limiter’s model bounds out of its code. Its amendment changed none of the 17 statements ratified earlier, so only the code changed: the factory rewrote the limiter as a class whose capacity and queue size are passed in.

Its receipt, on #30, says the code is tested against the model in all 19,489 states. It marks one size larger as not claimed, because TLC didn’t finish the bigger model within its three minutes.

The same morning, the live dashboard’s count called every merge proved. The TypeScript merges are tested against the model, so #32 changed the label to “merged through the gate”, which every merge is, so the dashboard claims no more than the receipts do.

Two coding agents

Invariant runs Claude Code or Codex. An issue’s Agent: line picks one, or its project’s manifest does, and every record of the work names the agent that did it.

Codex’s commands run under a permission profile of their own: they read only the workspace and their tools, write only in the workspace, reach no network, and can’t read the home directory, where Codex keeps its sign-in.

Codex’s first build, on September 29, was two-phase commit: 28 steps in about 10 minutes, and the code is proved at every size.

That evening it built two parts of Invariant’s own decision journal, both proved at every size too: the store’s journal only grows, and a decision’s state is the fold of its journal’s lines. All 145 of Invariant’s decisions fold on the proved core as they are. Wiring the first part in found a real bug: the store kept lines unique by their hash alone, so a line another project had written word for word, in the same second, was dropped.

codex Two-phase commit its first build

invariant/gate · proved at every size · 288 states, and 1,568 one size larger Receipt

✓ Pass. Every check passed. The code is proved at every size. Fingerprint sha256:1ec3ecccde20

Coding agent: codex. The fingerprint leaves it out.

CheckResultEvidence
Pinned statements✓ 6 of 6 matchratified by @gitdek on #65, amending D-0027
Design · TLC✓ no violations, no deadlock288 distinct states (1,146 generated), depth 11
Reachability✓ 2 of 2 witnesses reachedAllCommitted in 10 steps, AllAborted in 3 steps
Known bugs✓ 1 of 1 caughtearly-commit: TCConsistent violated after 5 steps
Agreement✓ code reaches the model's states288 states, depth 11
One size larger✓ code reaches the model's states1,568 states, depth 14, within RM = {r1, r2, r3, r4}
Code · Gobra✓ proved: 9 of 9 functions verified9 with contracts, overflow checked, not verified: Init, transactionManager, withTransactionManager, Try, modelValue, phaseName, Abstract
Code · conformance✓ tested against the model: every reachable state, no step outside it4,896 steps recorded, 288 of 288 model states visited
Every step tried✓ in every state reached, but where only the environment's bounds rule a step out4,896 attempts in 288 states, refusals included
Build✓ go vet, go testsandboxed, no network

Checked within RM = {r1, r2, r3}, and again one size larger, within RM = {r1, r2, r3, r4}. Within each, TLC's search is exhaustive. Gobra proves the code against its contracts at every size, and the design's rules are claimed only within the sizes checked.

codex Prove the store's journal only grows (#177, part 4) #199

invariant/gate · proved at every size · 144 states, and 200,000 one size larger Receipt

✓ Pass. Every check passed. The code is proved at every size. Fingerprint sha256:1f484c2b2a9e

Coding agent: codex. The fingerprint leaves it out.

CheckResultEvidence
Pinned statements✓ 9 of 9 matchratified by @gitdek on #195
Design · TLC✓ no violations, no deadlock144 distinct states (397 generated), depth 9
Reachability✓ 2 of 2 witnesses reachedKeptAbandoned in 2 steps, RebuiltFromOther in 3 steps
Known bugs✓ 3 of 3 caughtrebuild-replaces: StoreOnlyGrows violated after 2 steps, abandon-drops: StoreOnlyGrows violated after 2 steps, write-not-journaled: KeepsEveryLine violated after 1 step
Agreement✓ code reaches the model's states144 states, depth 9
One size larger✓ code reaches the model's states200,000 states, depth 19, within Checkouts = {c1, c2, c3}, MaxLines = 3
Code · Gobra✓ proved: 6 of 6 functions verified6 with contracts, overflow checked, not verified: Init, restore, readSystem, Try, checkoutValue, lineSet, Abstract
Code · conformance✓ tested against the model: every reachable state, no step outside it1,584 steps recorded, 144 of 144 model states visited
Every step tried✓ in every state reached, but where only the environment's bounds rule a step out1,584 attempts in 144 states, refusals included
Build✓ go vet, go testsandboxed, no network

Checked within Checkouts = {c1, c2}, MaxLines = 2, and again one size larger, within Checkouts = {c1, c2, c3}, MaxLines = 3. Within each, TLC's search is exhaustive. Gobra proves the code against its contracts at every size, and the design's rules are claimed only within the sizes checked.

Codex built it in 31 turns and 15 minutes, and the gate passed on its fourth run.

codex Prove a decision's state is the fold of its lines (#177, part 2) #200

invariant/gate · proved at every size · 43 states, and 43 one size larger Receipt

✓ Pass. Every check passed. The code is proved at every size. Fingerprint sha256:5f0f06e76fa1

Coding agent: codex. The fingerprint leaves it out.

CheckResultEvidence
Pinned statements✓ 14 of 14 matchratified by @gitdek on #193
Design · TLC✓ no violations, no deadlock43 distinct states (83 generated), depth 4
Reachability✓ 3 of 3 witnesses reachedAgentProposedPersonRatified in 2 steps, TwoWayDecidedByAgent in 1 step, Superseded in 2 steps
Known bugs✓ 4 of 4 caughtagent-ratifies: OnlyPeopleRatify violated after 2 steps, agent-decides-one-way: OneWayNeverDecided violated after 1 step, ratify-again: RatifiedOnce violated after 2 steps, decide-again: FirstLineOnly violated after 2 steps
Agreement✓ code reaches the model's states43 states, depth 4
One size larger✓ code reaches the model's states43 states, depth 4, within Agents = {agent}, MaxLines = 4, People = {alice}
Code · Gobra✓ proved: 12 of 12 functions verified12 with contracts, overflow checked, not verified: Init, restore, snapshot, Try, abstractWriter, abstractDoor, abstractStatus, abstractLine, Abstract
Code · conformance✓ tested against the model: every reachable state, no step outside it1,032 steps recorded, 43 of 43 model states visited
Every step tried✓ in every state reached, but where only the environment's bounds rule a step out1,032 attempts in 43 states, refusals included
Build✓ go vet, go testsandboxed, no network

Checked within Agents = {agent}, MaxLines = 3, People = {alice}, and again one size larger, within Agents = {agent}, MaxLines = 4, People = {alice}. Within each, TLC's search is exhaustive. Gobra proves the code against its contracts at every size, and the design's rules are claimed only within the sizes checked.

Codex built it in 23 turns and 11 minutes, and the gate passed on its first run. An earlier build, before the gate limited Gobra, looped for most of an hour.

What it doesn’t do yet

Invariant is pre-alpha. Model checking is exhaustive only within the bounds each receipt states, and one size past them where a receipt says so; nothing is claimed outside them. TypeScript is tested against the model, not proved.

The log buffer’s model assumes the shipper knows whether a send succeeded. And the work on crashes isn’t finished: what’s left is two watchers running live for a day.

Current status

The factory works as its own GitHub bot. A watcher polls GitHub through the gh command-line tool, holds the repository’s lease while it acts, and hands the writing to AI coding agents. Invariant itself is written in Go.

Since September 29 the factory has been paused, by Joseph’s call, until it’s ready to run for real: it was making drafts, plans and reviews faster than he could take them. Until then, coding agents build changes by hand, through pull requests that still pass the gate.

Its live dashboard is public: the factory’s orbit, the issues it’s working on, what it’s waiting for from a person, and its decision graph, every decision in the journal and what rests on what.

Watch it live The code on GitHub

More work

Have somethingin mind?

Tell me what you’re trying to run, fix, or automate. I reply within one business day.

Book a 20-minute call joe@puglisij.com