Our own repositories first
Every figure on this page comes from our own history, our own specifications, and our own substrate journal. The method was turned on ourselves before it was offered to anyone.
Governed execution · record
Three records,
one boundary.
A history report run on our own repositories, an exhaustive check of the authority and settlement boundary, and a bounded model of what more agents cost. Each record is dated, separates what a person checked from what a tool proposed, and names what it does not establish.
What the records show
Found, proven, measured.
These figures describe dated records. None of them is a live status, a guarantee, or an audit of any repository but our own.
Three lost updates in 5,480 commits
Thirteen agents under one git identity. The history report found three merges where one agent’s work was dropped by another’s, one of them unnoticed for ten weeks, and a larger number of look-alikes a person ruled out.
Read the history record1,744,784 states, zero violations
Two independent model checkers agree exactly that, within stated bounds, no agent can settle an unauthorized or unevidenced operation through the governed path. The bounds and the gap to the running code are stated with the result.
Read the verification recordEfficiency 67% at two agents, 29% at six
In a bounded race model, rework per settlement grows superlinearly with fleet size while safety holds at every N. Coordination cost is measured, not assumed.
Read the envelope recordClaimed, candidates, not claimed
Each record keeps three columns apart: what a person checked and claims, what a tool proposed and no one has yet checked, and what was looked at and ruled out. Limits sit beside the figures, not in a footnote.
This page grants nothing
It is a projection of dated records. References name the records behind each figure; they are not public links. Nothing here changes what is true in the system it describes.
Recorded history report · scan of October 3, 2026
Where agents overwrote each other.
Three times, in our own history.
Before offering the history report to anyone else, we ran it on our own main repository: 5,480 commits from 13 agents, all committing under one git identity. The method finds commits that dropped lines another agent added in the previous seven days, apparently without having seen them. A tool proposes candidates; a person checks every claimed item against the history.
What the record claims
Three agent-on-agent lost updates, all on one day of bulk merging, plus a larger number of look-alikes that a person had to rule out. Neither repository is free of collisions; neither shows a pattern of agents silently overwriting each other.
- Commits scanned
- 5,480Main product repository, October 31, 2025 to October 3, 2026. A second repository (2,157 commits, 2 agents) was scanned the same way and produced no claimed loss.
- Agents
- 13One shared git identity. Agents were told apart by the 644 declared work branches their changes arrived through.
- Claimed lost updates
- 5 findings in 3 mergesTwo checked in detail, one a minor documentation loss. All three merges happened on July 25, 2026.
- Longest unnoticed loss
- 13 lines · 10 weeksBuild-configuration guidance dropped on July 25 and missing from main until the report found it. Restored October 3, 2026.
- Messages with no sender identity
- 627 of 2,731 · 23%Messages dispatched to our agents between September 27 and October 3, 2026, with no session or agent recorded.
- Commits under a placeholder identity
- 4630 matched a --no-verify command, so commit hooks did not run. The other 16 are merge commits whose hook status is unverified.
- Claimed
- Five findings in three merges. Each passed three checks by hand: the merged file equalled one parent's file wholesale; the symbols the work branch introduced were present on that branch and absent after the merge; the dropped lines exist nowhere else in the tree, so a move is not counted as a loss.
- Candidates
- Sixteen findings in six commits are listed and not claimed: deliberate record-keeping merges, the same fix landing twice, a rebase that kept the earlier work. A second pass that labels agents from merge messages found 14 findings in 7 merges; those have not yet been checked by hand, so the real count may be higher.
- Not claimed
- 156 adjacent overwrites: later commits that removed another agent's recent lines while that change was already in their history. Ordinary iteration on shared files. Zero explicit reverts of another agent's commit in either repository.
- Limits
- History only: force-pushes, resets and deleted branches leave no trace in a clone. Lines of text are matched, not meaning, so a legitimate rewrite can look like lost work. Author-time ordering selects candidates; it is a heuristic, not proof of what an agent had seen. Attribution depends on how work is labelled.
Inspect the evidence and its limits
Availability and verification describe the records behind this entry. References name records in the source environment; they are not public links and this page is not a live status.
Can the findings be reproduced?
- Availability
- available
- Verification
- checked
The report reads git history only (log, diff, blame) on a private copy and does not change the repository. The redacted sample names every claimed item, every candidate, and the reason each candidate was not claimed.
Stomp history report · redacted dogfood sample · scan of 2026-10-03stomp-audit 0.2.2 · settled source commit 5531e5f3
Who checked the claimed findings, and how?
- Availability
- available
- Verification
- checked
A person, with the three checks above. The method compares author times rather than committer times because a bulk replay resets committer times, and it calls its automatic tier candidates, never findings.
Sample report · Method and Limits sections
Were the attribution and hook-skip counts reviewed the same way?
- Availability
- partial
- Verification
- reported
The message-identity and placeholder-commit figures come from the same setup's dispatch and commit records. A regex scan of the 30 hook-skipping commits found no secrets; that was a quick check, not a security review.
Offer background table · 2026-09-27 to 2026-10-03
Is the private evidence available to a reviewer?
- Availability
- partial
- Verification
- reported
Hashes, paths and agent identities are held privately and can be shown to a customer's reviewer on request, in a form we choose. The public sample anonymises agents to role labels and paths to file types.
Sample report · header
What this record does not establish
- What an agent knew or intended. Author-time ordering picks candidates for a person to judge; it does not establish awareness.
- Anything about hosts, clones or CI pipelines the live checks were not installed on.
- A final count. The stomp definition is a draft pending review, and the second pass has unchecked candidates.
- Anything about anyone's repository but our own.
Recorded model check · October 29, 2026
No agent can settle without authority and evidence.
Two checkers, no shared code, exact agreement.
The authority and settlement lifecycles — the small trusted boundary between agent reasoning and governed effects — are written as TLA+ specifications and checked exhaustively over every reachable state of bounded models. Two independent model checkers run identical inputs. Verdicts, distinct-state counts and search depths must agree exactly, or the claim is blocked.
What the record claims
Within the stated bounds and assumptions, no conflicting or unauthorized operation can reach settled finality through the governed execution path. The model may decide anything; the boundary decides which effects are admissible.
- Distinct states · deep settlement model
- 1,744,7843 operations, epoch ≤ 4. 21,464,617 states generated, depth 39, zero invariant violations. Both checkers report the same distinct count.
- Distinct states · small models
- 25,676 · 10,168Authority (2 agents, 2 resources, 2 nonces) and settlement (2 operations, epoch ≤ 3). Depths 12 and 26. Both checkers exact.
- Counterexamples
- 0Across all runs. The first run surfaced one artificial terminal state from the finite epoch horizon; it was handled by configuration, not by weakening the specification.
- Independent checkers
- 2TLC, the reference oracle, and tla-mc, a Rust checker. A disagreement on any future run blocks the claim.
- Deep-model check time
- 12.7 s · ~40 stla-mc and TLC respectively, TLC at 10 workers. The two engines are run for agreement, not speed.
- Claimed
- Authority: every commit is backed by a grant issued in its own epoch and unexpired at commit; no two active leases on one resource; each nonce commits at most once. Settlement: an operation that is settled or closed had authority at land and the full evidence set; settlement happens only against current ancestry; closure needs all three journal marks. All hold on every reachable state of the models listed.
- Candidates
- The deep authority model (3 agents, 3 resources, epoch ≤ 4) is pending. Liveness — that work eventually settles under fairness — is not yet modeled. Symbolic checking for wider bounds is the next track.
- Not claimed
- Implementation correspondence. These are models of intended behavior. The running system enforces the same transition guards, and three known gaps between specification and code are written down. A conformance harness that replays real work records against the specifications is the next tier, named rather than implied.
- Limits
- Bounded models, not arbitrary size. No Byzantine agents: adversarial means arbitrary interleaving and failure timing, not forgery inside the enforcement boundary. The quality of evidence content is outside the model.
Inspect the evidence and its limits
Availability and verification describe the records behind this entry. References name records in the source environment; they are not public links and this page is not a live status.
Can the result be reproduced?
- Availability
- available
- Verification
- checked
Both specifications, all models and both checkers run from one task file; the checker is fetched on first run. Raw logs are committed next to the report.
nabi-verify · verification report · 2026-10-29model-check-results · settlement-deep.log · settlement-deep-rust.log
What interleavings did the checkers explore?
- Availability
- available
- Verification
- checked
Lease expiry against commit; custody loss between expiry and re-grant; epoch advancement mid-flight; duplicated nonce delivery; authority revocation between land and settle; main advancing under an in-flight operation, forcing a rebase; a crash at every non-terminal point; retry re-entry.
verification report · Adversarial coverage
Where is the boundary enforced in the running system?
- Availability
- available
- Verification
- reported
Three interlocked layers: a git reference-transaction hook that rejects non-fast-forward, direct and anonymous updates to main; a freeze-approval binding that hash-binds gate receipts and re-validates them at settle; and the specifications that model the guards the first two enforce.
cto-diligence · enforcement boundaryimplementation-map · known correspondence gaps
Is there a live surface?
- Availability
- partial
- Verification
- reported
A loop re-checks the small models and regenerates a dashboard on a cadence. This page is a dated snapshot of that record, not the live surface and not a status report.
nabi-verify · report · run history
What this record does not establish
- That the implementation is correct. Specification-to-code correspondence is mapped, not proven.
- Behavior beyond the modeled bounds, or under partition semantics outside the lease and epoch assumptions.
- Anything about agent reasoning or the quality of what an agent decides.
Recorded model ladder · October 29, 2026
More agents is not free.
Safety holds at every N. Efficiency does not.
A bounded race model: N operations compete, each settlement advances the epoch and strands its peers on a stale base, and each stranded peer pays a rebase. Goodput is settlements; cost is rebases. Both are read from the checker's action-coverage counts and cross-checked by the two engines agreeing on distinct states at every N.
What the record claims
In the idealized race, rework per settlement grows superlinearly with fleet size while every safety invariant continues to hold. Coordination cost is measured in the model, not guessed.
- Efficiency · N = 2
- 67%4 settlements, 2 rebases. Efficiency is settlements divided by settlements plus rebases.
- Efficiency · N = 6
- 29%79,326 settlements, 194,880 rebases. 141,463 distinct states, identical on both checkers.
- Rework per settlement
- 0.5 → 2.46From N = 2 to N = 6, rising monotonically: 0.5, 0.89, 1.29, 1.84, 2.46.
- Invariant violations
- 0Settled-fresh and settled-monotone hold at every N. Both engines agree on distinct counts at every N.
- Governance rejections · live journal
- 1,351 of 15,722 eventsOne four-day substrate window, May 27 to 30, 2026. Protective policy denials — pressure on the boundary — not collisions.
- Claimed
- The shape of the curve under the model's assumptions, and exact agreement between two checkers on distinct states at N = 2 through 6.
- Candidates
- Operational contention in the running system — re-port churn, holds, rebases — is recorded. It is a different signal from state-space growth and from agents acting on stale beliefs; joining the three is open work.
- Not claimed
- A production optimum. If only rework is counted, the model's optimum is trivially one agent. Real systems weight wall-clock goodput against rework, and the weight depends on the workload and on which agents run together, not only how many.
- Limits
- An idealized race in which every settlement strands every peer; real conflict graphs are sparser. The journal window is one four-day sample from May 2026.
Inspect the evidence and its limits
Availability and verification describe the records behind this entry. References name records in the source environment; they are not public links and this page is not a live status.
Can the ladder be reproduced?
- Availability
- available
- Verification
- checked
One task runs N = 2 through 6 on both checkers and writes one record per N with settlements, rebases, distinct counts and whether the engines agreed.
nabi-verify · contention ladder recordspecs · ConcurrencyCost.tla
What does the live journal show?
- Availability
- partial
- Verification
- reported
15,722 substrate events over four days: 5,719 dispatch liveness beats, 1,351 access rejections under policy, 720 completed sessions, nine kinds of agent. The rejections are protective denials and are not evidence of agents overwriting each other.
nabi-verify · operational journal record · 2026-05-27 to 2026-05-30
What this record does not establish
- That the system is faster, or slower, with more agents. Efficiency here is a model ratio, not a measured throughput.
- That any specific fleet size is safe or unsafe in production.
- A relationship between the model curve and the live journal. They are presented side by side, not joined.
From record to repository
Start with one repository.
The history report ran on our own repositories before anyone else's. A scoped, observe-only run on one repository is how we would begin with yours: it reads history, records what a strict policy would have refused, blocks nothing, and ends in a written report that says what it could and could not see.