docs: Proven/Witnessed/Trusted ladder; correct believe_me and annotation claims

.claude/CLAUDE.md

@@ -35,7 +35,7 @@ exceptions:
 
 | Layer | Language | Role |
 |---|---|---|
-| **ABI** | **Idris2** | Formally verified contract — dependent-type proofs, state machine or exposure-gate invariants, `%default total`, zero `believe_me`/`postulate`/`assert_total` in the trusted core. |
+| **ABI** | **Idris2** | Formally verified contract — dependent-type proofs, state machine or exposure-gate invariants, `%default total`, no `postulate`/`assert_total`, and `believe_me` only in the 4 documented `SafetyLemmas` axioms (core) — zero in cartridge ABIs. |
 | **FFI** | **Zig** | C-ABI implementation (ADR-0006 five-symbol pattern: `boj_cartridge_{init,deinit,name,version,invoke}`). |
 | **Adapter** | **Zig** | The base-level API/service surface — see below. |
 

Justfile

@@ -415,7 +415,7 @@ fmt-check:
     @echo "Checking Zig formatting..."
     find ffi/ -name '*.zig' -exec zig fmt --check {} +
 
-# Lint — verify zero believe_me + type-check all ABI files
+# Lint — trusted-base audit (only the 4 sanctioned axioms) + type-check all ABI files
 lint: verify-no-believe-me typecheck
     @echo "Lint passed!"
 
@@ -434,15 +434,15 @@ typecheck:
 # Verify the trusted base: no unsound constructs beyond the sanctioned axioms.
 #
 # The estate trusted-base reduction policy (hyperpolymath/standards#203) sanctions
-# EXACTLY the 5 class-(J) axioms in src/abi/Boj/SafetyLemmas.idr — opaque Char/String
+# EXACTLY the 4 class-(J) axioms in src/abi/Boj/SafetyLemmas.idr — opaque Char/String
 # primitives, %unsafe-tagged and externally validated (see PROOF-NEEDS.md and
 # docs/proof-debt.md). Everything else must be a genuine constructive proof.
 # This recipe fails on any believe_me/assert_* outside that module, and also
 # fails if the audited axiom count drifts from 5 (keep the docs in sync).
 verify-no-believe-me:
     bash scripts/check-trusted-base.sh
 
-# Full verification suite: type-check + zero believe_me + build + test
+# Full verification suite: type-check + trusted-base audit + build + test
 verify: typecheck verify-no-believe-me build test
     @echo "Full verification passed!"
 
@@ -616,7 +616,7 @@ deps-audit:
     echo "Running Zig build + test audit on catalogue..."
     cd ffi/zig && zig build test
     cd "$OLDPWD"
-    # Verify zero believe_me (formal verification soundness audit)
+    # Trusted-base audit (formal verification soundness audit)
     just verify-no-believe-me
     # Supplementary scanners (if available)
     if command -v panic-attack >/dev/null 2>&1; then
@@ -1410,7 +1410,7 @@ tour:
     echo "Quick commands:"
     echo "  just run         Start server (REST 7700, gRPC 7701, GraphQL 7702)"
     echo "  just test        Run all FFI tests"
-    echo "  just verify      Full verification (typecheck + zero believe_me)"
+    echo "  just verify      Full verification (typecheck + trusted-base audit)"
     echo "  just matrix      Show cartridge capability matrix"
     echo "  just test-smoke  Quick smoke test"
     echo ""
@@ -1449,7 +1449,7 @@ help-me:
     echo "  just readiness        Component Readiness Grade tests"
     echo "  just bench            Run benchmarks"
     echo "  just integration      End-to-end integration tests"
-    echo "  just verify           Full verification (typecheck + zero believe_me + build + test)"
+    echo "  just verify           Full verification (typecheck + trusted-base audit + build + test)"
     echo "  just typecheck        Type-check all Idris2 ABIs"
     echo "  just verify-no-believe-me  Scan for unsound constructs"
     echo ""

PROOF-NEEDS.adoc

@@ -1,13 +1,13 @@
 == PROOF-NEEDS.md — boj-server
 
 ____
-*See also*: link:docs/proof-debt.md[`+docs/proof-debt.md+`] is the
+*See also*: link:docs/proof-debt.adoc[`+docs/proof-debt.adoc+`] is the
 schema-conformant per-repo index under the estate
 https://github.com/hyperpolymath/standards/blob/main/docs/TRUSTED-BASE-REDUCTION-POLICY.adoc[Trusted-Base
 Reduction Policy] (standards#203, enforcement standards#211).
 PROOF-NEEDS.md is the _strategic-goals_ narrative — full audit table,
 classification rationale, and external-validation pointers.
-`+docs/proof-debt.md+` is the _machine-checked_ index that
+`+docs/proof-debt.adoc+` is the _machine-checked_ index that
 `+scripts/check-trusted-base.sh+` greps. Keep both in sync when the
 marker count in `+src/abi/Boj/SafetyLemmas.idr+` changes.
 ____
@@ -51,7 +51,7 @@ run over nothing.
 *exactly 4* sanctioned class-(J) axioms in `+SafetyLemmas.idr+`, zero
 undocumented unsound constructs. (`+charEqSym+` was discharged
 2026-06-24, taking the count 5 → 4; `+EXPECTED_AXIOMS=4+` in the
-enforcing script is the source of truth, and `+docs/proof-debt.md+`
+enforcing script is the source of truth, and `+docs/proof-debt.adoc+`
 agrees.) Independently corroborated by a `+panic-attack assail+` scan
 (MPL-2.0, built from source), which flags the same `+believe_me+` sites
 as `+ProofDrift+` and nothing else proof-shaped.
@@ -114,7 +114,7 @@ historically.
 are documentation/comment mentions of the word (1 in SafeHTTP.idr line
 15, 1 in SafetyLemmas.idr line 9, 2 in
 cartridges/fleet-mcp/abi/FleetMcp/SafeFleet.idr lines 14 & 34) and are
-*not* axiom uses. The audited true count is 5.
+*not* axiom uses. The audited true count was 5; it is 4 since 2026-06-24.
 * *LOC*: ~5,400 (Elixir + Idris2)
 * *ABI layer*: Comprehensive dependent-type ABI
 
@@ -323,3 +323,26 @@ validating `+prim__eqChar+` / `+prim__strToCharList+` /
 then citing that evidence here. This is a backend-assurance task, not a
 proof obligation — keep it tracked but do not expect a constructive
 proof.
+
+=== Model-to-code obligations (added 2026-10-06)
+
+The proofs above are about the Idris model. These obligations connect the
+model to the running server; README "What is proven" summarises where each
+claim sits today.
+
+. *Restore the proof gate.* `idris2 --typecheck boj.ipkg` fails because
+  `allTake` is defined twice in `SafetyLemmas.idr`; the `proofs.yml`
+  typecheck job fails at `asdf install idris2 ""` and is path-skipped on
+  most PRs. Delete the duplicate, pin the Idris2 version, remove the skip.
+. *Every bound foreign symbol exists (Obligation B).* Each
+  `%foreign "C:<sym>,<lib>"` in `src/abi/Boj/` resolves to a symbol in a
+  library `ffi/zig/build.zig` builds. Today 13 of the 17
+  `boj_safety_*` bindings to `libbozsafety` have no implementation and the
+  library is not a build target. Add a CI check (`nm` over the built
+  artefact, with a planted-positive control) and implement or delete each
+  binding.
+. *Effect-typed tool manifests (Obligation C).* Declare each MCP tool's
+  effect once (`Read | Write | Delete | Exec`) in Idris, generate the
+  `mcp-bridge/lib/tools.js` annotations from it with a CI drift check,
+  have the dispatcher enforce it, and prove that a `Read` tool's dispatch
+  targets contain no mutating action, with no new axioms.

README.adoc

@@ -34,6 +34,7 @@ ____
 * link:#transports[Transports]
 * link:#configuration[Configuration]
 * link:#security[Security]
+* link:#what-is-proven[What is proven]
 * link:#license[License]
 * link:++#contributing--links++[Contributing & links]
 
@@ -49,7 +50,7 @@ ____
 * *Inspectable offline* — `boj++_++health`, `boj++_++menu`, `boj++_++cartridges`, and `boj++_++cartridge++_++info` answer from an offline manifest so clients can introspect the server without any backend running.
 * *MCP resources & prompts* — 7 `boj://` resources and reusable prompts (`audit-repo`, `convene-cluster`, `deploy-with-dns-ssl`, `summarize-channel`, `triage-issues`, `proof-status`).
 * *Hardened* — per-call rate limiting, size caps, prompt-injection detection with Unicode-confusable normalisation, and error sanitisation (paths, stack traces, and env vars stripped from responses).
-* *Formally verified core* — the coordination ABI is written in Idris2 with discharged proof obligations; remaining axioms are documented, not hidden.
+* *Formally verified ABI model* — an Idris2 safety and dispatch ABI (HTTP, CORS, API keys, WebSocket lifecycle, prompt injection, catalogue, dispatch, credential isolation), `%default total`, with four documented axioms and nothing else unsound. Proofs are about the Idris model; see link:#what-is-proven[What is proven] for where they stop.
 
 '''''
 
@@ -258,7 +259,7 @@ Key environment variables (full schema in link:glama.json[`glama.json`]):
 * *Error sanitisation* — responses strip filesystem paths, stack traces, and environment variables before they reach the client.
 * *HTTP safety* — `BOJ++_++HTTP++_++AUTH=none` is refused on any non-loopback bind; bearer auth is required for remote exposure.
 * *Credential isolation* — cartridge credentials are supplied per-cartridge (env vars or the `vault-mcp` broker), never embedded in tool definitions.
-* *Formal verification* — the coordination ABI safety layer is written in Idris2 with discharged proof obligations; remaining `believe++_++me` sites are isolated, documented axioms over the compiler's opaque `Char`/`String` primitives, tracked in link:PROOF-NEEDS.md[`PROOF-NEEDS.md`].
+* *Formal verification* — the Idris2 ABI safety layer has discharged proof obligations; the only `believe++_++me` sites are four documented axioms over the compiler's opaque `Char`/`String` primitives, tracked in link:PROOF-NEEDS.adoc[`PROOF-NEEDS.adoc`]. See link:#what-is-proven[What is proven] for the Proven / Witnessed / Trusted breakdown.
 * *Supply chain* — SHA-pinned GitHub Actions; coherence tests assert the advertised tool list matches the cartridge manifest so nothing is advertised-but-undispatched.
 
 Run the coherence tests:
@@ -272,6 +273,37 @@ Report vulnerabilities per link:SECURITY.md[`SECURITY.md`].
 
 '''''
 
+== What is proven
+
+Every safety claim BoJ makes sits in one of three bins. "Proven" always means _proven about a model_, so the claim is only as good as the match between that model and the running code. That is why the Witnessed column matters.
+
+[cols="1,1,1",options="header"]
+|===
+|Proven — the compiler checks it |Witnessed — an artefact backs it |Trusted — relied on from outside
+
+a|
+* *Status (2026-10-06): the core does not currently typecheck.* `SafetyLemmas.idr` defines `allTake` twice, and the CI typecheck job has not completed since at least 2026-09-21 (it fails while installing Idris2, and is path-skipped on most PRs). Tracked in link:https://github.com/hyperpolymath/boj-server/issues/343[#343]. Until that is fixed, read this column as "proven when last green", not "proven now".
+* The Idris2 ABI in `src/abi/Boj/` (17 modules, all `%default total`) covers catalogue and dispatch, HTTP/CORS/API-key/WebSocket/prompt-injection safety predicates, and the credential-isolation model.
+* `believe++_++me` appears only in *four* documented axioms over opaque `Char`/`String` primitives (`SafetyLemmas.idr`); CI (`scripts/check-trusted-base.sh`) pins that count and greps the rest of the Idris tree for `believe++_++me`, `assert++_++total`, `assert++_++smaller` and `idris++_++crash`. The grep has known gaps (a use followed by a `--` comment is skipped; `partial`, `covering` and holes are not scanned) and the job is path-filtered, so it does not run on every PR.
+* *Limit:* these proofs are about the Idris model. The model is only ever typechecked, never compiled or linked into the running server, and 13 of the 17 C safety checks it binds (`libbozsafety`) are not yet implemented.
+a|
+* Property tests (Elixir StreamData, `elixir/test/backend_assurance/`) of the behaviour each of the four axioms assumes, run against Elixir analogues of the Chez primitives (not the compiled Idris code); last executed and green 2026-10-06.
+* Zig FFI enum constants checked at compile time against a hand-kept mirror of the Idris values (the Idris side itself is not compared).
+* TLA+ specs of the JS worker, worker pool and invoker (`specs/elixir-harness/`), model-checked with TLC by hand (results recorded in its README), not in CI.
+* npm package published with provenance; SLSA level 3 provenance on release tarballs; container build attestation.
+* Coherence tests: the advertised tool list matches the dispatch table.
+a|
+* The JavaScript bridge (`mcp-bridge/`) and the Zig FFI: the proofs cover the model, not this code.
+* Tool annotations (`readOnlyHint`, `destructiveHint`, …): hand-written labels, not derived from types and not enforced at dispatch.
+* Postgres, Docker, cloud and forge APIs behaving as documented; cartridge backends you run yourself.
+* The Idris2 compiler, Zig, the Node/Deno/Bun runtime and the operating system.
+* The AI choosing the right tool. Prompt injection is limited by input hardening, not proven away.
+|===
+
+Planned next steps that move items left (Trusted → Witnessed → Proven) are tracked in link:PROOF-NEEDS.adoc[`PROOF-NEEDS.adoc`]: link every bound C symbol and gate CI on it, and derive tool annotations from a typed effect declaration that the dispatcher enforces.
+
+'''''
+
 == License
 
 * *Code* — link:LICENSE[MPL-2.0] (Mozilla Public License 2.0) — the license published to npm and detected by GitHub.

README.md

@@ -31,6 +31,8 @@
 
 - [Security](#security)
 
+- [What is proven](#what-is-proven)
+
 - [License](#license)
 
 - [Contributing & links](#contributing--links)
@@ -53,7 +55,7 @@
 
 - **Hardened** — per-call rate limiting, size caps, prompt-injection detection with Unicode-confusable normalisation, and error sanitisation (paths, stack traces, and env vars stripped from responses).
 
-- **Formally verified core** — the coordination ABI is written in Idris2 with discharged proof obligations; remaining axioms are documented, not hidden.
+- **Formally verified ABI model** — an Idris2 safety and dispatch ABI (HTTP, CORS, API keys, WebSocket lifecycle, prompt injection, catalogue, dispatch, credential isolation), `%default total`, with four documented axioms and nothing else unsound. Proofs are about the Idris model; see [What is proven](#what-is-proven) for where they stop.
 
 # Install
 
@@ -242,7 +244,7 @@ Key environment variables (full schema in [`glama.json`](glama.json)):
 
 - **Credential isolation** — cartridge credentials are supplied per-cartridge (env vars or the `vault-mcp` broker), never embedded in tool definitions.
 
-- **Formal verification** — the coordination ABI safety layer is written in Idris2 with discharged proof obligations; remaining `believe_me` sites are isolated, documented axioms over the compiler’s opaque `Char`/`String` primitives, tracked in [`PROOF-NEEDS.md`](PROOF-NEEDS.md).
+- **Formal verification** — the Idris2 ABI safety layer has discharged proof obligations; the only `believe_me` sites are four documented axioms over the compiler’s opaque `Char`/`String` primitives, tracked in [`PROOF-NEEDS.adoc`](PROOF-NEEDS.adoc). See [What is proven](#what-is-proven) for the Proven / Witnessed / Trusted breakdown.
 
 - **Supply chain** — SHA-pinned GitHub Actions; coherence tests assert the advertised tool list matches the cartridge manifest so nothing is advertised-but-undispatched.
 
@@ -254,6 +256,51 @@ node --test mcp-bridge/tests/
 
 Report vulnerabilities per [`SECURITY.md`](SECURITY.md).
 
+# What is proven
+
+Every safety claim BoJ makes sits in one of three bins. "Proven" always means *proven about a model*, so the claim is only as good as the match between that model and the running code. That is why the Witnessed column matters.
+
+<table>
+<colgroup>
+<col style="width: 33%" />
+<col style="width: 33%" />
+<col style="width: 33%" />
+</colgroup>
+<thead>
+<tr>
+<th style="text-align: left;">Proven — the compiler checks it</th>
+<th style="text-align: left;">Witnessed — an artefact backs it</th>
+<th style="text-align: left;">Trusted — relied on from outside</th>
+</tr>
+</thead>
+<tbody>
+<tr>
+<td style="text-align: left;"><ul>
+<li><p><strong>Status (2026-10-06): the core does not currently typecheck.</strong> <code>SafetyLemmas.idr</code> defines <code>allTake</code> twice, and the CI typecheck job has not completed since at least 2026-09-21 (it fails while installing Idris2, and is path-skipped on most PRs). Tracked in <a href="https://github.com/hyperpolymath/boj-server/issues/343">#343</a>. Until that is fixed, read this column as "proven when last green", not "proven now".</p></li>
+<li><p>The Idris2 ABI in <code>src/abi/Boj/</code> (17 modules, all <code>%default total</code>) covers catalogue and dispatch, HTTP/CORS/API-key/WebSocket/prompt-injection safety predicates, and the credential-isolation model.</p></li>
+<li><p><code>believe_me</code> appears only in <strong>four</strong> documented axioms over opaque <code>Char</code>/<code>String</code> primitives (<code>SafetyLemmas.idr</code>); CI (<code>scripts/check-trusted-base.sh</code>) pins that count and greps the rest of the Idris tree for <code>believe_me</code>, <code>assert_total</code>, <code>assert_smaller</code> and <code>idris_crash</code>. The grep has known gaps (a use followed by a <code>--</code> comment is skipped; <code>partial</code>, <code>covering</code> and holes are not scanned) and the job is path-filtered, so it does not run on every PR.</p></li>
+<li><p><strong>Limit:</strong> these proofs are about the Idris model. The model is only ever typechecked, never compiled or linked into the running server, and 13 of the 17 C safety checks it binds (<code>libbozsafety</code>) are not yet implemented.</p></li>
+</ul></td>
+<td style="text-align: left;"><ul>
+<li><p>Property tests (Elixir StreamData, <code>elixir/test/backend_assurance/</code>) of the behaviour each of the four axioms assumes, run against Elixir analogues of the Chez primitives (not the compiled Idris code); last executed and green 2026-10-06.</p></li>
+<li><p>Zig FFI enum constants checked at compile time against a hand-kept mirror of the Idris values (the Idris side itself is not compared).</p></li>
+<li><p>TLA+ specs of the JS worker, worker pool and invoker (<code>specs/elixir-harness/</code>), model-checked with TLC by hand (results recorded in its README), not in CI.</p></li>
+<li><p>npm package published with provenance; SLSA level 3 provenance on release tarballs; container build attestation.</p></li>
+<li><p>Coherence tests: the advertised tool list matches the dispatch table.</p></li>
+</ul></td>
+<td style="text-align: left;"><ul>
+<li><p>The JavaScript bridge (<code>mcp-bridge/</code>) and the Zig FFI: the proofs cover the model, not this code.</p></li>
+<li><p>Tool annotations (<code>readOnlyHint</code>, <code>destructiveHint</code>, …): hand-written labels, not derived from types and not enforced at dispatch.</p></li>
+<li><p>Postgres, Docker, cloud and forge APIs behaving as documented; cartridge backends you run yourself.</p></li>
+<li><p>The Idris2 compiler, Zig, the Node/Deno/Bun runtime and the operating system.</p></li>
+<li><p>The AI choosing the right tool. Prompt injection is limited by input hardening, not proven away.</p></li>
+</ul></td>
+</tr>
+</tbody>
+</table>
+
+Planned next steps that move items left (Trusted → Witnessed → Proven) are tracked in [`PROOF-NEEDS.adoc`](PROOF-NEEDS.adoc): link every bound C symbol and gate CI on it, and derive tool annotations from a typed effect declaration that the dispatcher enforces.
+
 # License
 
 - **Code** — [MPL-2.0](LICENSE) (Mozilla Public License 2.0) — the license published to npm and detected by GitHub.

docs/RSR_OUTLINE.adoc

@@ -38,7 +38,7 @@ just typecheck
 # Run tests
 just test
 
-# Full verification (zero believe_me + type-check + tests)
+# Full verification (trusted-base audit + type-check + tests)
 just verify
 ----
 
@@ -52,7 +52,7 @@ Every cartridge follows the ABI/FFI universal standard:
 
 |**ABI**
 |Idris2
-|Formal proofs, `%default total`, zero `believe_me`
+|Formal proofs, `%default total`, `believe_me` only in 4 documented axioms
 
 |**FFI**
 |Zig

docs/developer/README.adoc

@@ -8,7 +8,7 @@
 
 A cartridge is a swappable, formally verified capability module. It occupies one or more cells in the 2D matrix (protocol x domain) and follows the three-layer stack:
 
-. *Idris2 ABI* — Type-safe interface with `%default total` and zero `believe_me`
+. *Idris2 ABI* — Type-safe interface with `%default total`; `believe_me` only in 4 documented core axioms
 . *Zig FFI* — C-compatible native execution
 . *zig Adapter* — REST + gRPC + GraphQL endpoints