# Invariant proof audit: the second pass, at the test files

`docs/2026-08-23-invariant-proof-audit.md` classified every contract in

`INVARIANTS.md` as specific or universal and repaired nineteen proofs that

could not fail for their claims. It also recorded its own limit: most verdicts

"were judged from the mechanism the contract names rather than re-derived. A

second pass over those would be worth doing and is not what this one did."

This document is that second pass. Every contract's cited proof was read at

the file — the test, the script, the migration, and the production module it

claims to cover — and checked against issue #166's mechanical test: name a

violation the proof would not catch. Line numbers refer to the working tree on

2026-08-24.

The first pass asked whether a universal claim's population is closed. This

pass asks a different question about the same proofs: when the claim is

violated, does the named proof actually go red? Five defect classes recur:

1. **Fixture-path assertions.** The test asserts on a fixture, a hand-built

   map, or a JSON file's own fields rather than the production path.

2. **Subset coverage.** The proof examines some members of the claimed

   population — two adapters of four, one extension object of four, one route

   of a class.

3. **Shared-code tautologies.** The expected value is computed by the code

   under test, so a bug moves both sides together and the assertion holds.

4. **Vacuous assertions.** The assertion is true by construction — an element

   ID that exists nowhere, a literal read back from the module that hard-codes

   it, an immutability property every BEAM value has.

5. **Empty-input passes.** An enumeration or scan that matched nothing passes

   as if it had checked everything, with no positive control forcing it to

   find what it should find.

## Result

130 contracts, one verdict each.

| Verdict | Count |

| --- | --- |

| Can fail — the proof goes red when the claim is violated | 61 |

| Partial — the core clause bites, but named clauses have no proof that can | 57 |

| Cannot fail — a load-bearing clause has no proof that can go red | 12 |

One proof is red right now, and that is the mechanism working: see the next

section. The verdicts here are about the cited proofs as they exist; "partial"

is not a defect report against the code, and several "cannot fail" entries

cover code that is currently correct. The finding in each case is that nothing

executable would notice when it stops being correct — which is the exact

condition `INVARIANTS.md` lines 13-25 names as the companion to taxonomy

rule 7.

## The proof that is failing right now

`ADMIN-001`'s enumerating proof, `test/openagents_web/operator_surface_test.exs`,

is statically red at HEAD. Commit `310dac1` ("Open the Gym", an ancestor of

HEAD) added:

- `/gym`, classified `:operator` with scope `gym:read` at

  `lib/openagents_web/route_authority.ex` lines 192-193, absent from the

  declared operator-route table at `test/openagents_web/operator_surface_test.exs`

  lines 33-72;

- `OpenAgentsWeb.GymLive` (lines 21 and 30) and `OpenAgentsWeb.GymRunController`

  (line 46), both calling `OpenAgents.Accounts.admin?/1`, absent from the

  declared authority-module table at lines 76-104.

`ADMIN-001` does not name the Gym anywhere. The proof is doing exactly what

#146 built it to do — a new operator surface fails until the contract is

amended to name it — and the failure reached `main` anyway. That is a process

finding, not a proof finding: the commit's own message reports a scoped test

run, and the section below on the gate shows how a candidate can carry a

`passed` receipt without this file ever running. The fix is two-sided: amend

`ADMIN-001` to name the Gym read surface, and close the gate path that let a

red enumeration land.

## Proofs that cannot fail for a load-bearing clause

Each entry names the claim, the cited proof, the violation the proof cannot

catch, and the smallest change that would let it fail.

### MEMORY-005 — the tests assert the violating behavior

**Claim:** `memory_remember.v1` accepts only a claim directly authorized by

the current user message, a host-recorded confirmation, or a first-party UI

action; "model arguments cannot substitute."

**Reality:** `lib/openagents/tools/memory_remember.ex` lines 130-135 swallow

every `OpenAgents.Memory.Consent` failure and proceed with

`%{kind: "conversation_context"}` — the model's arguments are the write

authority. The cited proof encodes this as correct:

`test/openagents/tools/profile_memory_tools_test.exs` lines 240-262 store a

model-paraphrased claim under `consent_kind == "conversation_context"`, and

lines 292-307 store a claim that **differs from** the exact confirmation on

record ("I prefer concise answers" confirmed, "I prefer detailed answers"

stored) and assert success. The `Consent` unit tests (lines 22-119) prove the

strict module in isolation; no test runs the tool with a fabricated claim and

asserts refusal.

**Smallest change:** delete the `{:error, _} -> %{kind: "conversation_context"}`

fallback so the tool returns the consent error, or amend MEMORY-005 to say

what the code does — a conversation-context write authorized by topical

relevance, not by exact consent. Either way the current sentence and the

current code cannot both stand.

### RELEASE-003 — the cited proof tests dead code

**Claim:** invalid, insecure, or path-bearing origins fail startup.

**Reality:** `OpenAgentsWeb.AllowedOrigins` has no production caller — the

only references in the repository are its own file and its test. Production

origin checking is `config/runtime.exs` line 190 feeding `check_origin` at

line 545, validated by `lib/openagents/runtime_config.ex` lines 823-840.

`test/openagents_web/allowed_origins_test.exs` therefore tests a module you

can delete without changing production behavior, and `ops/ci/release-smoke.sh`

never opens a WebSocket or sends an `Origin` header (lines 99-114 curl

`/health` over plain loopback HTTP), so the "production WebSocket read-back"

in the evidence line has no executable artifact.

**Smallest change:** either route `config/runtime.exs` through

`OpenAgentsWeb.AllowedOrigins.for_production/2` so the tested module is the

production path, or retarget the proof at `OpenAgents.RuntimeConfig`'s origin

validation and delete the dead module.

### VOICE-005 — the disclosure assertion checks an element that exists nowhere

**Claim:** while recording is on, the surface that carries `START VOICE`

states before the microphone opens that calls are recorded; a visible marker

announces capture while running.

**Reality:** `test/openagents_web/live/chat_live_test.exs` line 206 asserts

`refute has_element?(view, "#voice-recording-disclosure")` — an ID that

appears nowhere else in the repository, so the assertion cannot fail under any

change. The positive disclosure is proven only on the memory surface

(`test/openagents_web/controllers/data_controller_test.exs` lines 243-247

against `lib/openagents_web/live/memory_live.ex`), while the surface that

carries `START VOICE` (`lib/openagents_web/live/chat_live.ex` line 2069)

renders no disclosure text. The capture marker at line 2063 is

`visually-hidden` and referenced by no test. The teardown half is also

unclosed: `assets/test/voice_state_test.mjs` lines 55-71 call the teardown

function directly with fakes; nothing proves `destroyed()` or reconnect

actually calls it (`assets/js/voice_controller.js` line 501 is the one call

site).

**Smallest change:** assert the disclosure element that the chat surface

actually renders — which first requires the chat surface to render one — and

delete the impossible-ID refutation.

### MODULE-004 — the proof is a JSON fixture identity check

**Claim:** every capability surface preserves the same authority boundary;

external effects need receipts; oversized catalogs degrade to discovery;

missing executors fail honestly.

**Reality:** `test/openagents/surface_eval_test.exs` is 28 lines. Lines 13-18

assert that the case IDs in `priv/sarah/evals/surfaces/identity-authority.v1.json`

equal a hard-coded list. Three of the four corpus cases — external effect

under read authority, oversized catalog, unavailable executor — declare

expectations that nothing executes. The file never touches

`OpenAgents.Modules.SurfacePolicy`, `OpenAgents.Tools.Registry`, or

`OpenAgents.Tools.Runner` — the three modules the invariant names as

evidence. Renaming a corpus case turns the test red; an external effect

executing under read-only authority does not.

**Smallest change:** drive the three unexecuted corpus cases through

`OpenAgents.Tools.Runner`, or narrow MODULE-004's proof index row to the

surface-vocabulary and revalidation tests in

`test/openagents/modules/router_test.exs` (lines 107-134), which do bite.

### COLLECTIVE-002 — the leak scanner has zero coverage

**Claim:** generalizer output "is scanned again for secrets, contacts,

identifiers, paths, exact source fragments, authority-bearing fields, and

size before storage."

**Reality:** the scanner exists (`lib/openagents/collective/generalizer.ex`

lines 267-299, five reject branches including the four-gram quote detector)

and no test reaches any reject branch — a grep for the rejection reasons

across `test/` returns nothing. The leak assertions in

`test/openagents/collective_generalizer_test.exs` lines 38-48 run against a

payload built from fixed-vocabulary maps that no input text ever flows into,

so they are true by construction.

**Smallest change:** construct a payload carrying a source fragment and

assert `validate_payload/2` rejects it — one test per reject branch.

### IDENTITY-006 — the branch discipline is enforced but never tested

**Claim:** Git receive-pack authorizes every requested ref update; the

assignment credential can update only its assignment branch, never a default

or protected branch.

**Reality:** nothing in `test/` exercises `authorize_receive_pack/3` or

`allowed_assignment_ref?/3` (`lib/openagents/forge/git_http.ex` lines

303-329). Deleting the default-branch and protected-branch checks fails no

test. `test/openagents/forge/assignment_test.exs` lines 133-147 test pkt-line

parsing — the input to the decision, not the decision. The non-Git-API

refusal in the auth plug is likewise untested, and the "stores only a digest"

assertion at lines 96-97 is tautological (the schema has no plaintext field

to leak).

**Smallest change:** a receive-pack push with an assignment credential

against the default branch, over the same real-HTTP harness

`test/openagents/forge/push_closes_issues_test.exs` already stands up,

asserting refusal — plus one against the assignment branch asserting success.

### DEPLOYPLANE-004 — "the only definition" has no only-ness proof

**Claim:** `OpenAgents.Deployments.Lifecycle` is the only definition of legal

states and transitions, enforced transactionally.

**Reality:** the transitions themselves are well proven

(`test/openagents/deployments/lifecycle_test.exs` lines 12-18 quantify over

the transition table), but nothing enumerates writers of run state — no

compiled-import-table assertion like FLEETPROMOTE-001's, and no PostgreSQL

transition trigger on the runs table (contrast `work_jobs`, whose trigger

`test/openagents/work_job_test.exs` line 232 exercises). The suite itself

demonstrates the bypass: `test/openagents/issues/completion_claims_test.exs`

lines 565-571 force a run to `succeeded` with a raw update.

**Smallest change:** either a transition trigger on the runs table with a

raw-update test, or a dependency-boundary assertion that the lifecycle module

is the sole caller of the state-writing function.

### OBSERVABILITY-001 — the read-back is proven against an empty database

**Claim:** release read-back recomputes zero-tolerance leakage, consent,

provenance, executor-disclosure, and attribution checks from authoritative

records without selecting private content.

**Reality:** `test/openagents/observability_test.exs` line 52 runs

`OpenAgents.Observability.Readback` against a freshly sandboxed database with

no conversation, message, or memory row seeded. The

"contains no private content" refutations (lines 65-66) are vacuous — there

is no content to leak — and the all-planes-healthy loop (lines 59-63) passes

over empty status maps. The blocked case is manufactured with `put_in` rather

than by seeding a violation, so neither direction (detects a real violation;

excludes real content) is exercised. The emit half does bite, but only 2 of 6

refusal branches are tested (lines 22-48).

**Smallest change:** seed one conversation with a known sentinel string and

one zero-tolerance violation, then assert the read-back reports the violation

and the sentinel appears nowhere in the snapshot.

### RELEASE-001 — nothing can fail when migrations stop preceding traffic

**Claim:** the production image runs all pending migrations before starting

the HTTP server.

**Reality:** the evidence line names the Docker `CMD`, but the `CMD` contains

no migration step — the ordering lives in `lib/openagents/application.ex`

lines 22-24 behind `migrate_on_boot`, which

`lib/openagents/runtime_config.ex` lines 267-268 require in staging and

production. No test asserts that requirement (the only `migrate_on_boot` hit

in `test/` is a fixture setting it true), and

`test/openagents_web/controllers/health_controller_test.exs` runs against an

already-migrated test database. The smoke boots the release, but health is

`SELECT 1` (`lib/openagents_web/controllers/health_controller.ex` line 5),

which succeeds on an unmigrated database, and the smoke never verifies the

database is fresh. Remove the migration call and every cited proof stays

green.

**Smallest change:** a `test/openagents/runtime_config_test.exs` case

asserting staging and production refuse `migrate_on_boot: false`, and a

migration-sensitive probe in the smoke (query a table the newest migration

creates). Also correct the evidence line: the mechanism is

`OpenAgents.Release` invoked from the application start, not the `CMD`.

### RELEASE-002 — the absence half has no detector

**Claim:** secrets are absent from source, the build context, and image build

arguments.

**Reality:** `ops/ci/reference-check.sh` is a naming check, not a secret

scan, and it cannot fail even at its own job when `rg` is missing: lines 37

and 39 end in `|| true`, and `ops/ci/gate.sh` line 71 checks for `jq mix npm`

but never `rg`, so on a builder without ripgrep the check silently passes.

Nothing reads `.gitignore` or `.dockerignore` in any test; nothing scans

`config/` or the Dockerfile for credential material; the Cloud Logging

exclusion the contract names exists only as prose in `INVARIANTS.md`. The

GitHub-config half (`test/openagents/github_oauth/runtime_config_test.exs`)

does bite, narrowly.

**Smallest change:** fail `ops/ci/reference-check.sh` when `rg` is absent

(and add it to the gate's tool check), and add a repository-tree scan test

for high-signal secret shapes in `config/` and the Docker build context —

the same read-the-repo shape `test/openagents/hosted_ci_absence_test.exs`

already uses.

### UI-003 — no population of surfaces exists to enumerate

**Claim:** product surfaces render only through the sanctioned component

library.

**Reality:** `test/openagents_web/component_catalog_test.exs` proves the

catalog page documents the components — the arrow points the wrong way — and

`test/openagents_web/ui_test.exs` proves the primitives behave. Nothing scans

surfaces: a new LiveView rendering hand-rolled markup with its own palette

passes every cited proof. The narrow template scan that exists

(`test/openagents_web/ui_contracts_test.exs`) checks inert-control rules

only, by design.

**Smallest change:** narrow the claim to what the proofs cover (the primitive

contracts and the catalog), or add a template scan over

`lib/openagents_web/**` asserting variant-bearing markup uses the sanctioned

class-plus-data-attribute shapes.

### DATA-001 — the projection-loss clause has no test

**Claim:** losing PubSub or the LiveView stream must not lose accepted data;

rows are persisted before their state is presented as accepted.

**Reality:** the cited tests prove `create_turn/2` persists and a happy-path

turn renders (`test/openagents/conversations_test.exs` lines 28-41,

`test/openagents_web/live/chat_live_test.exs` lines 536-589). Nothing kills

a subscription, drops a stream, or asserts persist-before-broadcast ordering,

so a regression to broadcast-then-persist passes.

**Smallest change:** narrow the claim to what the tests prove (durable rows

for accepted turns), or add an ordering assertion at the delta-persistence

seam.

## Claims the code or the tests contradict

These are prose defects: the proof is fine or repairable, but the sentence in

the ledger is not what the system does.

- **VOICE-006 and VOICE-009** both state "sending typed input while voice is

  active ends the voice generation first." The cited test proves the

  opposite by design: `test/openagents_web/live/chat_live_test.exs` lines

  282-342 is titled "typing during a live voice call keeps the call open and

  hands voice the message" and asserts the session stays `listening`. The

  no-parallel-responses property may still hold through injection (no text

  turn opens), but the stated mechanism is a superseded design.

- **DATA-002** credits "unique indexes and identity-source constraint in

  `create_github_users`." No migration by that name exists — the indexes live

  in `priv/repo/migrations/20260816214200_create_sarah_conversations.exs` —

  and no identity-source constraint exists at all: nothing prevents a

  visitors row carrying both a browser key and a user ID. No test inserts a

  duplicate or races two creates, so dropping the unique indexes also fails

  nothing.

- **ADMIN-001** says the `/admin` panel shows recording completeness

  metadata; `test/openagents_web/live/admin_live_test.exs` lines 110-119

  refute recording strings with a stale comment claiming the product does not

  capture call audio, and line 139's model-ID refutation is vacuous because

  no call is seeded.

- **IDENTITY-007**'s proof index row cites `test/openagents/agents_test.exs`,

  which contains no grant test; the lifecycle is actually proven in

  `test/openagents/forge/assignment_test.exs` lines 105-131 and the two

  controller suites. The index row should follow the tests that exist.

- **STACK-001** cites `ops/ci/stack-contracts.sh` as evidence; nothing

  invokes it — it appears in no gate stage and wraps the same test file the

  suite already runs.

- **RELEASE-001**'s "Evidence: Docker `CMD`" points at a command with no

  migration step (see above).

- **MEMORY-003**'s evidence line lists `test/openagents/profile_memory_test.exs`

  twice — cosmetic.

## Tautologies, wrong chokepoints, and unexercised constraints

The most consequential "partial" verdicts, each with the violation the proof

misses.

### THREAD-001 — the race proof does not race

`test/openagents/threads/credit_race_test.exs` line 20 is

`use OpenAgents.DataCase, async: false`, and `test/support/data_case.ex`

line 40 starts the sandbox owner in shared mode for non-async tests. Every

`Task.async_stream` worker therefore serializes on one shared connection —

the concurrent opens and mints are savepoints on a single transaction, not

competing transactions. Deleting both `FOR UPDATE` locks in

`lib/openagents/threads.ex` (the admission-cap lock and the mint-side lock)

leaves all four tests green, and THREAD-001's amended text cites this file as

proving "the cap holds under concurrency." The token-reach half of THREAD-001

(`test/openagents/threads/grant_token_reach_test.exs`) is the strongest

enumeration in the repository — four derived sets, both directions, explicit

non-emptiness guards, route population from the router. The race clause needs

a test that checks out two real connections (unsandboxed or with explicit

allowances) before it proves anything.

### REPUTATION-001 — verification shares the producer's canonicalization

Every signature and digest check verifies with the same

`OpenAgents.Provenance.Canonical` encoding that produced the claim

(`test/openagents/reputation_test.exs` lines 38 and 45-49;

`lib/openagents/reputation/claim.ex` lines 103 and 112). A canonicalization

bug — a dropped field, an unstable ordering — verifies fine on both sides.

The tamper test (lines 116-124) catches a signature that ignores content, not

an encoding that ignores a field. "No function returns a ranking" is one

`function_exported?` check on one name (line 93) with no enumeration of the

module's exports. The key-rotation half

(`test/openagents/forge/key_rotation_test.exs`) bites hard and is the model

to follow. Smallest change: pin one full claim to a hard-coded expected byte

encoding and digest, the way `test/openagents/forge/wal_test.exs` lines

282-298 pin the WAL encoding.

### TOOL-005 — the boundary is enumerated at the wrong chokepoint

`test/openagents/dependency_boundary_test.exs` lines 152-178 enumerate

callers of `OpenAgents.Tools.Selector` and require each to name

`OpenAgents.Tools.Reach`. But `OpenAgents.Tools.Registry` is itself a public

un-narrowed catalog builder — `lib/openagents/tools/registry.ex` line 135

forwards whatever options it was handed — and the real catalog builders sit

one hop out (`lib/openagents/turns/turn_server.ex` line 113,

`lib/openagents/work/job_server.ex` line 138), outside the enumeration. A new

caller of the registry's prompt-definitions functions that omits `:reach`

offers the whole catalog and stays green — the exact violation the contract

says this test catches. The "names Reach" check is also satisfied by the

registry's unrelated boot-time `Reach.requirements()` call

(`lib/openagents/tools/registry.ex` line 366), so it cannot distinguish

resolving a caller from mentioning the module. Smallest change: enumerate

callers of the registry's catalog-building functions and require the reach

option at those sites.

### SELF-EDIT-001 — the population is a namespace prefix and the assertion is vacuous on empty

`test/openagents/dependency_boundary_test.exs` lines 196-198 filter to

modules named under the tools namespace, but the contract quantifies over

"every tool module." A tool-shaped module elsewhere — the coding work module,

a future plugin namespace — can name the hot-loader and stay green. The

assertion at line 93 is `offenders == []`, which passes if the module

enumeration breaks and returns nothing (unreadable BEAMs are swallowed at

line 210), and the fleet-release module list at lines 43-50 is hand-declared

with no existence check, so a renamed release module silently empties the

check forever. Smallest change: assert the enumerated population and the

release-module list are both non-empty, and derive the tool population from

the shipped-plus-fixture catalogs rather than a name prefix.

### SETTLEMENT-001 — the uniqueness ladder is never climbed

Every "pays once" mechanism is a constraint no test reaches: the payment-hash

unique index (`priv/repo/migrations/20260823060000_create_bounty_settlement.exs`

line 147) cannot collide because the test gateway returns a constant hash and

no second payment ever succeeds; the single-`paid`-intent partial index and

the one-receipt-per-intent index are shadowed by earlier context refusals.

The invariant calls its schemas "seven append-only schemas," and no

append-only trigger exists on any settlement table — the refund test re-reads

a receipt and finds it unchanged, but nothing would have refused a rewrite.

Smallest change: raw-insert tests against each uniqueness constraint, and

either add the append-only triggers or strike the phrase.

### COMPENSATION-001 — the payout check reads back a literal

"Never creates payout authority" is proven by

`refute function_exported?(..., :payout, 2)` and by asserting

`payout_authority == false` in a projection that hard-codes the literal

(`lib/openagents/compensation.ex` lines 30, 205, 239). The real defense — the

database CHECK on the policy rules

(`priv/repo/migrations/20260817010500_create_compensation_accounting.exs`

line 162) — is never bitten, and only one of seven append-only triggers is

tested. Smallest change: insert a policy with `payout_authority: true` raw

and assert PostgreSQL refuses.

### EFFECT-001 — the production call site's transaction is untested

The outbox mechanics bite (`test/openagents/effects_test.exs`: real rollback,

real payload-digest conflict, real reclaim, genuinely concurrent claims). But

`test/openagents/effects/work_launch_test.exs` lines 27-41, titled "commits

its launch in the same transaction," asserts only that the effect exists

afterward, and the refusal case fails before the enqueue runs — so moving the

enqueue outside the job transaction, reintroducing the exact crash window

EFFECT-001 exists to close, keeps both tests green. The two schema

constraints the contract leans on (`effects_lease_pair_check`,

`effects_status_shape_check` in

`priv/repo/migrations/20260824204740_create_effects.exs`) are never reached

by any test. EFFECT-002's milestone separation therefore also rests on

untested constraints. Smallest change: a raw insert against each constraint,

and a work-launch test that crashes between the job insert and the launch and

asserts the effect row exists.

### MODULE-001 — the pre-invocation byte check is real and unproven

The runner verifies the loaded executor before invocation

(`lib/openagents/tools/registry.ex` line 190), but the only tamper test

mutates an in-memory struct and calls the verify helper directly

(`test/openagents/modules/registry_test.exs` lines 171-184). Delete the

runner's check and the suite passes; no test unloads or changes module bytes

and drives the runner. Smallest change: purge a tool module's code in a test

and assert the runner returns the unavailable outcome.

### EXIT-005 — the sole-writer clause and the publisher

The chain, the rewrite mutation, and the anchor checks are excellent — the

rewrite is a real byte-level rewrite with recomputed keys, and the stranger's

anchor is taken from served bytes. Two clauses still have no proof:

- **"`append_entry/2` is the one function every writer reaches the log

  through"** — unchanged since the 2026-08-23 audit recorded it (issue #151).

  No test enumerates WAL writers, and the escape is real: `append_entry/2` is

  pure; the durable write is the CAS, and the test suite itself writes

  indexes without the chain in four places in

  `test/openagents/forge/independence_test.exs`. On a log with a pre-contract

  prefix, a bypassing writer's `chain_link_missing` is classified as history

  (`lib/openagents/forge/verification.ex` lines 330-341), so the bypass can

  be absorbed silently. The current writer population is three modules

  (`lib/openagents/forge/pushes.ex` line 175, `lib/openagents/forge/git_plane.ex`

  line 532, `lib/openagents/repositories/importer.ex` line 450); an

  import-table enumeration in the shape of

  `test/openagents/threads/grant_token_reach_test.exs` would close it.

- **`OpenAgents.Forge.AnchorPublisher` has zero test coverage.** Every anchor

  test calls the publish function by hand; nothing proves the scheduled child

  runs, reschedules, or that `published_at` advances — the clause the

  contract says lets a reader see that publication has stopped. Removing the

  supervisor child fails nothing.

Also: the encoding is verified by the same module that produces it;

`test/openagents/forge/wal_test.exs` lines 282-298 mitigate this with a

pinned hard-coded digest, which is the right shape and worth extending to a

full entry-plus-link vector.

### EXIT-002 and EXIT-003 — depth-1 import tables and a hand-listed function set

The independence reads are strict about missing modules (a `MatchError`, not

an empty pass), but they read one module's own import table only: a helper

module between the verifier and the database, or an `apply/3`, is invisible.

The mirror-function refusal at `test/openagents/forge/independence_test.exs`

line 564 names three functions as a literal with no completeness assertion

against the pushes module's exports — a new mirror-reading export evades it.

### EXIT-001 — six probes accept 200 with an empty body

`read_probe/2` (`test/openagents/data_rights/export_inventory_test.exs`

lines 529-534) treats any 200 as portable without checking the body, so the

six families the contract narrates as previously blocked would still read

portable if their routes regressed to returning empty lists for the owner's

own records. The issue, project, and repository probes check for the seeded

record; these six should too.

### WORK-001 — two of three bounds and the resume claim

The tool-call ceiling bites; the continuation ceiling and the ten-minute wall

clock have no test (no hit for either reason code in `test/`). The

non-advertisement clauses (no `deep_work` in a job's provider request, no

`work.delegate` or `memory.write` authority) are structurally invisible to

the scripted provider, which ignores the tools field entirely. Recovery

"resumes and continues" is asserted only as "not interrupted, generation

advanced" — a worker that adopts and immediately fails passes. SCV-001

inherits the same shape: "no job may deploy one" (`scv.deploy` never in job

authorities) has no test.

### Route classification — the catch-alls and the operator class

`test/openagents_web/authenticated_route_gate_test.exs` is the real thing —

derived population, non-empty guard, actual anonymous dispatch. Two

structural gaps sit beside it. First, the classifier's catch-alls

(`lib/openagents_web/route_authority.ex` line 588 for API GETs, lines 695-724

for browser path shapes) classify unknown reads as `:public_read` silently —

a private GET added in one of those shapes leaves the gate population without

failing anything; the box fan-out status route already demonstrates the

mislabel (harmless today only because the API inventory independently

dispatches it). Second, no test dispatches `:operator` routes anonymously as

a class — the gate test filters them out, and

`test/openagents_web/operator_surface_test.exs` proves membership, not

behavior, checking `pipe_through` for exactly one route. A route correctly

classified and correctly listed, but wired without the operator pipeline and

without an in-handler recheck, passes everything. FLEETPROMOTE-001's

`/admin/forge` is one path-keyed classification away from that shape, saved

today by its own LiveView test. Smallest change: dispatch the operator class

anonymously the way the authenticated class is dispatched.

### Scope-boundary scans — one backend is invisible and one guard is missing

`test/openagents/memory/scope_boundary_test.exs` is two proofs of different

strength. The entry-point enumeration bites. The query scan does not guard

against emptiness on the recall side (line 196 iterates whatever the AST scan

returns), and `OpenAgents.Memory.HybridRecall` reaches the database only

through raw SQL the AST scan cannot see — deleting the conversation predicate

from `lib/openagents/memory/hybrid_recall.ex` line 70 fails nothing. The scan

also accepts a scope column named anywhere in the query, not only in a

`where`. Separately, `OpenAgents.Memory.SemanticIndex.rebuild/1`

(`lib/openagents/memory/semantic_index.ex` lines 120-126) reads messages

across every conversation and sits outside both MEMORY-001's and MEMORY-004's

populations. And PRIVACY-001's projector enumeration labels

`OpenAgents.Tools.MemoryContract` as reading the category list only, while

its `memory_output/1` returns the raw stored claim to the model with no

redaction pass (`lib/openagents/tools/memory_contract.ex`) — the one-projector

assertion at line 264 compares the declaration to itself, and the redaction

check at line 270 is satisfied by any mention of the redaction module.

### UI-002 — the AST matcher's syntax blind spot

`test/openagents_web/tool_activity_projection_test.exs` has real anti-vacuity

guards and both-direction key sets, but its matcher recognizes only

`from ... select:` keyword queries; a projection written as a pipeline

(`select/3`, `select_merge`, a `Map.take` after the query) lands in neither

set and the exactness still passes.

### PERSONA-001 — two adapters have no wire probe

The behaviour and atom-table enumerations bite in both directions. But of the

three outbound HTTP adapters, only one is driven against a capturing plug;

`OpenAgents.Providers.OpenRouter` and `OpenAgents.Providers.VercelGateway`

have no wire probe in the boundary file, the configured-provider backstop

reads test-double config rather than production selections, and the

gateway's config key is not in the checked set. An OpenRouter payload builder

that appended its own system text would pass. (The payload test that exists

covers the messages field only, and shows instructions are trimmed — so

"byte for byte" is already not literal there.)

### PROVIDER-002 — lane routing is unverifiable under test config

The refusal paths bite against the production catalog list. But all three

provider lanes are the same test module under `config/test.exs`, so the

adapter-lane assertions are `Test == Test`, and the catalog endpoint tests

compare the response to the same function that renders it.

## The gate itself

Findings that are about whether proofs run, not whether they can fail.

- **A Markdown-only candidate runs no tests.** `ops/dev/precommit.sh` lines

  61-81 skip the test suite when every changed path is documentation, and

  `ops/ci/gate.sh` line 116 runs precommit as a stage — the receipt still

  records the stage as passed. Tests with no dedicated gate stage are only

  reached through precommit, including

  `test/openagents/hosted_ci_absence_test.exs`,

  `test/openagents/network_status_test.exs`,

  `test/openagents_web/transparency_surface_test.exs`,

  `test/openagents/transparency/work_disclosure_test.exs`,

  `test/openagents/forge/deployment_lane_test.exs`,

  `test/openagents/capacity_test.exs`, and both token-vault suites. This is

  the most likely mechanism by which the red operator-surface enumeration

  reached `main`.

- **The gate receipt is forgeable and short-circuits.** `ops/ci/gate.sh`

  lines 15-30 and 51-54: an unsigned JSON at a known path skips the gate

  entirely. `test/openagents/forge/gate_receipt_test.exs` proves shape and

  SHA-binding, not authenticity — RELEASE-004 does not claim authenticity, so

  this is a bound to record rather than a defect, but the stage list is

  declared in three unlinked places and nothing ties the receipt's list to

  the script's.

- **`ops/ci/reference-check.sh` passes when `rg` is missing** (see

  RELEASE-002 above).

- **RELEASE-004's absence test covers hosted providers by list**, and the

  list omits `cloudbuild.yaml` — notable because the deployment target is

  Google Cloud — plus a handful of others (CodeBuild, Bitbucket, Gitea and

  Forgejo workflow paths).

- **VAULT-001's third vault has no test.** `OpenAgents.Voice.RecordingVault`

  has no test file; nothing proves it does not borrow the GitHub key, and no

  enumeration closes the vault population, so a fourth vault that borrows a

  key is invisible.

## Every contract, one verdict

Verdicts: **can fail** (the cited proof goes red when the claim is violated),

**partial** (the core clause can fail; the named clause cannot), **cannot

fail** (a load-bearing clause has no proof that can go red). Details above

where a section exists; one line here for everything else.

### Identity and canon

| Contract | Verdict | Sharpest gap |

| --- | --- | --- |

| CANON-001 | partial | Content SHA-256 is shape-checked, never compared to any file's bytes (`lib/openagents/persona/source_manifest.ex` line 256) |

| CANON-002 | can fail | Strongest enumeration in the set; pattern covers the public schema only, and the audit-kind check is one-directional |

| PERSONA-001 | partial | Two of three outbound adapters have no wire probe; config backstop reads test doubles |

| PERSONA-002 | can fail | Voice-session role receipt persistence has no cited proof |

| PERSONA-003 | partial | The incomplete-results branch is untested; corpus digest computed on both sides, so a weakened corpus moves both |

| BLUEPRINT-001 | partial | Deletion of admitted rows and the facts table never attempted; explicit-none pinned only at the composer layer |

| PROGRAM-001 | partial | No-effect-authority is four atom names on one module; the in-flight-capture test asserts BEAM immutability |

| DEGRADE-001 | can fail | Real trigger tests, default path covered |

| PROGRAM-002 | partial | "The live turn never consumes their result" has no test; the synthetic-corpus claim is the fixture describing itself |

| PROGRAM-003 | can fail | Generation-pointer proof is genuine |

### Identity and authorization

| Contract | Verdict | Sharpest gap |

| --- | --- | --- |

| IDENTITY-001 | can fail | One-time state, replay, ban, token-never-in-browser all driven |

| IDENTITY-002 | partial | Classifier catch-alls mislabel silently; Repo-reach scan has no positive control; public-read LiveViews exempt from the event hook |

| IDENTITY-003 | partial | Non-persistence is a schema field-name check; KDF envelope parameters unpinned |

| IDENTITY-004 | partial | One-active-link constraint and attribution-across-unlink untested |

| IDENTITY-005 | can fail | Route list is 5 of 12 box-control paths |

| IDENTITY-006 | cannot fail | See section above |

| IDENTITY-007 | partial | Cited file has no grant test; real coverage lives elsewhere |

| IDENTITY-008 | can fail | Lock asserted from the live database function; contention window honestly declared unproven |

| IDENTITY-009 | can fail | Planted-secret redaction is a real control |

| IDENTITY-010 | can fail | Catalog scan with positive control; nested-value and derived-copy residues |

| IDENTITY-011 | can fail | Query plan asserted with sequential scans priced out |

| IDENTITY-012 | can fail | Residue: a future non-changeset writer of guarded columns |

| CAPACITY-002 | can fail | Concurrency tests would fail without the locks |

| CAPACITY-003 | partial | Interval test asserts the literal it passed in; 15-second timeout and cost parser untested |

| WORK-002 | can fail | Single-probe and cancellation-stamp ordering proven |

### Data, memory, and privacy

| Contract | Verdict | Sharpest gap |

| --- | --- | --- |

| DATA-001 | cannot fail | See section above |

| DATA-002 | partial | Cited migration name and identity-source constraint do not exist; no duplicate-insert or race test |

| DATA-003 | can fail | Partition test is complete; timestamp-tie determinism unasserted |

| MEMORY-001 | can fail | The semantic-index rebuild reads cross-conversation and sits outside the population |

| MEMORY-002 | partial | Model-side clauses vacuous against a scripted provider; host-side halves bite |

| MEMORY-003 | can fail | Real trigger tests via raw SQL |

| MEMORY-004 | partial | Query scan vacuous for the hybrid backend's raw SQL; no non-empty guard on the recall side |

| MEMORY-005 | cannot fail | See section above |

| MEMORY-006 | partial | Synonym-recall metric measures the test's own regex provider |

| MEMORY-007 | can fail | Gate driven end to end with each bypass refused |

| MEMORY-008 | partial | Default-off asserted from the eval JSON, not the shipped config |

| MEMORY-009 | partial | Same default-off defect; build determinism genuinely proven |

| PRIVACY-001 | partial | The claim-projecting tool is mislabeled and skips redaction; projector assertion compares the declaration to itself |

### Turn, provider, and effects

| Contract | Verdict | Sharpest gap |

| --- | --- | --- |

| TURN-001 | can fail | Real second insert against the real index; no concurrent case |

| TURN-002 | partial | Single-transaction claim untestable as written — moving inserts out of the transaction passes |

| TURN-003 | partial | Non-blocking proven; persist-before-broadcast ordering not |

| TURN-004 | can fail | Idempotency claimed, never called twice |

| TURN-005 | partial | Parallel-call refusal and continuation ceiling have zero tests |

| PROVENANCE-001 | can fail | Five raw-SQL trigger tests; the strongest turn proof |

| PROVIDER-001 | partial | Contract test iterates two of four adapters |

| PROVIDER-002 | partial | Lane assertions are the same module compared to itself under test config |

| EFFECT-001 | partial | See section above |

| EFFECT-002 | partial | The status-shape constraint that carries the claim is untested |

| TOOL-001 | partial | No registry rebuild mid-turn; digest compared to the live registry |

| TOOL-002 | partial | Execution contexts hand-built rather than application-created |

| TOOL-003 | can fail | Claim atomicity proven sequentially only |

| TOOL-004 | partial | The UI disclosure test runs entirely on literal maps |

| TOOL-005 | partial | See section above — wrong chokepoint |

| TOOL-006 | can fail | Reads shipped config through the prod reader, not the test fixture; both directions |

| DEGRADE-002 | can fail | Honest-degradation asserted on the rendered answer |

### Collective, settlement, and modules

| Contract | Verdict | Sharpest gap |

| --- | --- | --- |

| COLLECTIVE-001 | partial | Cited database constraints never exercised; raw-quote check is six hand-listed fields |

| COLLECTIVE-002 | cannot fail | See section above |

| COLLECTIVE-003 | can fail | Append-only via real constraint errors |

| COMPENSATION-001 | partial | See section above |

| REPUTATION-001 | partial | See section above |

| SETTLEMENT-001 | partial | See section above |

| MODULE-001 | partial | See section above |

| MODULE-002 | can fail | Projection key allowlist would strengthen it |

| MODULE-003 | can fail | Nine-axis filter matrix is a real enumeration |

| MODULE-004 | cannot fail | See section above |

### Delegated work, threads, and deployment plane

| Contract | Verdict | Sharpest gap |

| --- | --- | --- |

| WORK-001 | partial | See section above |

| SELF-EDIT-001 | partial | See section above |

| SCV-001 | partial | The no-job-may-deploy clause has no test |

| OUTCOME-001 | partial | Four of five false-green classes never pass through either path; the pure-grader suite proves fixtures |

| THREAD-001 | partial | Token reach is exemplary; the race proof does not race (see above) |

| THREAD-002 | can fail | Write routes dispatched as a reader; one subset check is one-directional |

| DEPLOYPLANE-001 | partial | Artifact-digest format never validated |

| DEPLOYPLANE-002 | can fail | Every bound dimension widened in turn |

| DEPLOYPLANE-003 | partial | The digest half of "same SHA and same digest" never varied on the admission path |

| DEPLOYPLANE-004 | cannot fail | See section above |

| DEPLOYPLANE-005 | partial | Supervisor gating untested; all provider claims carried by the one fake |

| FLEETPROMOTE-001 | can fail | Best-proven contract in the ledger; the browser route's pipeline membership rests on its own LiveView test |

### Voice, admin, and interface

| Contract | Verdict | Sharpest gap |

| --- | --- | --- |

| VOICE-001 | can fail | Architecture and provider values never given a bad case |

| VOICE-002 | partial | CSRF never omitted; SDP size ceiling untested; header check greps the variable name, not the value |

| VOICE-003 | partial | The database-constraint half is unproven; the one-active index has no test and the code path does not use it |

| VOICE-004 | can fail | Hostile provider frames through the real decoder |

| VOICE-005 | cannot fail | See section above |

| VOICE-006 | can fail | But the prose contradicts the cited test (see above) |

| VOICE-007 | can fail | Changed-identity refusal has no dedicated test |

| VOICE-008 | can fail | Exact durable terminal set asserted |

| VOICE-009 | can fail | Real chronology plus a real constraint error; same stale sentence as VOICE-006 |

| VOICE-010 | partial | The advisory-lock serialization claim has no concurrent test |

| VOICE-011 | partial | The event-kind field is a free-text channel no test constrains; the 64-event cap untested |

| VOICE-012 | can fail | The no-opt-out never-claim has no closing mechanism |

| ADMIN-001 | can fail | Red right now (see above); membership proven, class-wide behavior not |

| DATA-004 | can fail | Cascade seeded broadly with direct-delete refusals first; the voice-summary export branch is vacuous |

| UI-001 | partial | The operator class is never dispatched anonymously |

| UI-002 | can fail | Pipeline-syntax queries evade the matcher |

| UI-003 | cannot fail | See section above |

| LEADERBOARD-001 | can fail | Two named exclusions never seeded, so excluded vacuously |

| OBSERVABILITY-001 | cannot fail | See section above |

### Release, status, and transparency

| Contract | Verdict | Sharpest gap |

| --- | --- | --- |

| RELEASE-001 | cannot fail | See section above |

| RELEASE-002 | cannot fail | See section above |

| VAULT-001 | partial | The recording vault has no test; no enumeration over the vault population |

| RELEASE-003 | cannot fail | See section above |

| RELEASE-004 | partial | Provider path list omits the deployment target's own CI config file |

| RELEASE-005 | can fail | Empty-relup refusal is a real positive control |

| RELEASE-006 | can fail | Both directions of refusal at target and readiness |

| RELEASE-007 | can fail | Parses the real Dockerfile; one silent-skip seam when a variable is undeclared in a stage |

| RELEASE-008 | can fail | Runs the real OTP walk against the real running application |

| RELEASE-009 | can fail | Fail-closed in every direction; the file has no dedicated gate stage |

| STATUS-001 | can fail | Structs contribute one opaque key; degradation enumerated for one section only |

| CAPACITY-001 | partial | Redaction proven over nine hand-listed fields, no exact key set on the projection |

| TRANSPARENCY-001 | partial | The route population filter misses the anonymous JSON API entirely; the gate check proves a static reference, not a gated path |

### Repository, exit, and issues

| Contract | Verdict | Sharpest gap |

| --- | --- | --- |

| REPOSITORY-001 | can fail | The past insert-the-grant-yourself defect is genuinely closed; regex-evading join forms remain the residue |

| API-001 | partial | Governance covers one of four extension objects; one enum is written twice with nothing binding the copies |

| CONTRIBUTION-001 | can fail | Cross-binds the document to the router, both authorities, and the real push guard |

| REPOSITORY-002 | can fail | Executes the real script against real hostile remotes |

| REPOSITORY-003 | can fail | Real pushes, real cache deletion, real replay |

| EXIT-001 | can fail | Six probes accept 200 with an empty body (see above) |

| EXIT-002 | partial | Depth-1 import tables; helper-module indirection invisible |

| EXIT-003 | partial | Mirror-function list is a literal with no completeness check |

| EXIT-004 | can fail | Rebuilds the exact #179 failing shape and clones for real |

| EXIT-005 | partial | Sole-writer clause still unproven (#151); the anchor publisher has zero coverage (see above) |

| EXIT-006 | can fail | Gap list vacuous today in one direction, by honest construction |

| STACK-001 | can fail | The cited CI script is invoked by nothing |

| ISSUE-001 | can fail | Real pushes over real HTTP through the real auth plug |

| FORUM-001 | can fail | The source scan carries its own anti-rot control |

| ISSUE-002 | can fail | The lock-based no-clobber clause and the 200-body bound are untested |

| ISSUE-003 | can fail | Ambiguous-name and unsettled-name cases covered |

| ISSUE-004 | can fail | Crafted events from readers asserted to write nothing |

| PROMISE-001 | partial | The LIVE gate is proven on create, not on update into LIVE |

| PROMISE-002 | can fail | Proposed status; the append-only trigger is already exercised |

| NOTIFY-001 | partial | The "reveals nothing" clause has no proof — no schema enumeration, no content refutation anywhere in the cited tests |

| FORGEAPI-001 | can fail | Dispatches every envelope-classified route and pins the exact key set |

## What to fix first

1. **Amend ADMIN-001 for the Gym and re-run the enumeration** — the ledger is

   wrong today and the proof already says so.

2. **MEMORY-005** — decide whether the code or the sentence is right; the two

   cannot coexist. If the fallback stays, the invariant must be rewritten and

   the consent claim withdrawn.

3. **Close the gate's Markdown-only skip** or give the enumeration tests

   (operator surface, transparency surface, hosted-CI absence, work

   disclosure) a dedicated gate stage, so a red enumeration cannot land with

   a passing receipt again.

4. **RELEASE-003** — wire the tested module into production or retarget the

   proof; today the claim is carried by code nothing cited tests, and the

   cited test covers code nothing runs.

5. **THREAD-001's race** — a concurrency proof in shared sandbox mode proves

   serialization by the test harness, not by the lock. Two real connections

   or an honest narrowing.

6. **The unexercised constraint set** — settlement uniqueness and append-only,

   the effects lease-pair and status-shape checks, compensation's payout

   CHECK, the voice one-active index: each is one raw-SQL test in the shape

   `test/openagents/threads/grant_fence_test.exs` already uses everywhere.

7. **EXIT-005's writer set and publisher** — the one remaining row from the

   2026-08-23 audit's closing table, still open, plus a supervised child with

   no test.

8. **IDENTITY-006** — the credential's branch discipline is the whole point

   of the contract and is one real receive-pack test away from proven.

A closing observation the counts understate: the proofs this repository

builds when it decides to enumerate — the operator surface, the grant-token

reach, the visibility joins, the WAL rewrite, the fleet-promotion caller

sets — are genuinely strong, and three of them caught real defects during

this audit (the Gym, the mislabeled fan-out route, the stale admin-panel

comment). The recurring weakness is not the enumerations; it is the sentence

beside them that names a mechanism ("in one transaction", "under a lock",

"append-only", "the only definition", "before the supervision tree starts")

that no test has ever watched fail. Where a constraint or an ordering is

load-bearing, the proof should reach it raw — the way the fence, provenance,

and profile-memory tests already do — or the ledger should stop crediting it.