From 44cbd3baa736a77d9debfe79671563c5abe18a7a Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 6 Oct 2026 19:26:45 +0100 Subject: [PATCH 1/2] docs: Proven/Witnessed/Trusted ladder; correct believe_me and hint claims - README.adoc (+ regenerated README.md): new "What is proven" section with a three-column Proven / Witnessed / Trusted ladder. It states that the proofs are about the Idris model, which is typechecked but not linked into the running server; that 13 of 17 bound libbozsafety symbols have no implementation; and that the core does not typecheck today (duplicate allTake in SafetyLemmas.idr; the CI typecheck has not completed since at least 2026-09-21). Features/Security bullets no longer call it a "coordination ABI", and the PROOF-NEEDS link now points at the .adoc. - site/index.html: the "Verified" card becomes a compact ladder that links to the README section. - About 20 docs and the Justfile comments said "zero believe_me" or "5 axioms". The enforced budget is 4 sanctioned axioms in SafetyLemmas.idr (scripts/check-trusted-base.sh, EXPECTED_AXIOMS=4). Rules for cartridge authors ("your ABI must have zero believe_me") are unchanged. - PROOF-NEEDS.adoc: count history is 5 -> 4 (2026-06-24); fixed the broken docs/proof-debt.md links. - mcp-bridge/lib/tools.js: boj_browser_read_page and boj_browser_screenshot are now readOnlyHint:false, a conservative label until effect-typed manifests (PROOF-NEEDS Obligation C) land. boj_github_graphql (accepts mutations) and boj_cartridge_invoke (reaches any cartridge) are now destructiveHint:true. No A2ML files touched. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Ge6k9wanwVdYJWBrnwjPxf --- .claude/CLAUDE.md | 2 +- Justfile | 12 ++--- PROOF-NEEDS.adoc | 31 ++++++++++-- README.adoc | 36 +++++++++++++- README.md | 51 +++++++++++++++++++- docs/RSR_OUTLINE.adoc | 4 +- docs/developer/README.adoc | 2 +- docs/developer/llm-warmup-dev.adoc | 4 +- docs/developer/llm-warmup-user.adoc | 6 +-- docs/outreach/awesome-list-descriptions.adoc | 2 +- docs/outreach/blog-post-draft.adoc | 4 +- docs/outreach/show-hn-draft.adoc | 7 +-- docs/papers/boj-architecture-paper.adoc | 8 +-- docs/quickstarts/DEV.adoc | 2 +- docs/quickstarts/USER.adoc | 2 +- docs/wikis/Developer-Guide.adoc | 4 +- mcp-bridge/lib/tools.js | 12 ++--- site/index.html | 12 ++++- src/abi/Boj/SafeHTTP.idr | 3 +- src/abi/README.adoc | 2 +- verification/proofs/README.adoc | 10 ++-- 21 files changed, 166 insertions(+), 50 deletions(-) diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index bbe59d61..e40e37cb 100644 --- a/.claude/CLAUDE.md +++ b/.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. | diff --git a/Justfile b/Justfile index 808932d2..4667d55c 100644 --- a/Justfile +++ b/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,7 +434,7 @@ 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 @@ -442,7 +442,7 @@ typecheck: 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 "" diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 9012b4dc..d3e508d7 100644 --- a/PROOF-NEEDS.adoc +++ b/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:,"` 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. diff --git a/README.adoc b/README.adoc index 87ba5d44..0e082ef5 100644 --- a/README.adoc +++ b/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). 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. diff --git a/README.md b/README.md index 3d407ae4..b41394c4 100644 --- a/README.md +++ b/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. + + +++++ + + + + + + + + + + + + + + +
Proven — the compiler checks itWitnessed — an artefact backs itTrusted — relied on from outside
    +

  • 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). 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.

    • +
    +

  • 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.

    • +
    +

  • 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 [`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. diff --git a/docs/RSR_OUTLINE.adoc b/docs/RSR_OUTLINE.adoc index dd3e9859..fe4cdb9b 100644 --- a/docs/RSR_OUTLINE.adoc +++ b/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 diff --git a/docs/developer/README.adoc b/docs/developer/README.adoc index 23742ef9..bcd78376 100644 --- a/docs/developer/README.adoc +++ b/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 diff --git a/docs/developer/llm-warmup-dev.adoc b/docs/developer/llm-warmup-dev.adoc index 651ed9b6..0de05833 100644 --- a/docs/developer/llm-warmup-dev.adoc +++ b/docs/developer/llm-warmup-dev.adoc @@ -167,7 +167,7 @@ just run: == Idris2 ABI Conventions * *%default total* on all files -* *Zero believe_me* (enforced by `just verify-no-believe-me`) +* *No believe_me outside the 4 sanctioned SafetyLemmas axioms* (enforced by `just verify-no-believe-me`) * *IsUnbreakable proof*: only Ready cartridges pass * Package files: `*.ipkg` in each abi/ directory * Type-check: `idris2 --check --package boj boj.ipkg` @@ -281,7 +281,7 @@ See: `src/abi/Federation.idr`, `docs/FEDERATION.adoc` == Critical Invariants . Three-Layer Stack: every cartridge = Idris2 ABI + Zig FFI + Deno/JS `mod.js` -. Zero believe_me in all Idris2 sources +. No believe_me outside the 4 sanctioned SafetyLemmas axioms . %default total on all Idris2 files . IsUnbreakable: only Ready cartridges pass the proof . Hash attestation for community nodes diff --git a/docs/developer/llm-warmup-user.adoc b/docs/developer/llm-warmup-user.adoc index 80d724f6..44b3756c 100644 --- a/docs/developer/llm-warmup-user.adoc +++ b/docs/developer/llm-warmup-user.adoc @@ -12,7 +12,7 @@ formally verified interfaces. License: MPL-2.0. Author: Jonathan D.A. Jewell. == Architecture (30-second version) Every cartridge (except model-router-mcp) is a triple: -. *Idris2 ABI* — Dependent types proving correctness (zero believe_me) +. *Idris2 ABI* — Dependent types proving correctness (4 documented axioms, nothing else unsound) . *Zig FFI* — C-compatible .so shared library (5-symbol ADR-0006 ABI) . *Deno/JS adapter* — mod.js dispatched via JsWorkerPool (persistent pool) @@ -28,7 +28,7 @@ Three-class design: Class 1 (simple CLI), Class 2 (orchestrator), Class 3 (BEAM ---- just run # Start server (REST 7700) just test # Run all ExUnit + FFI tests -just verify # Full verification (typecheck + zero believe_me + build + test) +just verify # Full verification (typecheck + trusted-base audit + build + test) just test-smoke # Quick smoke test just matrix # Show cartridge capability matrix just doctor # Check toolchain @@ -89,7 +89,7 @@ and many more. == Invariants -* Zero believe_me in all Idris2 sources (currently 4 axiomatic primitives + logSafeBounded) +* No believe_me outside the 4 sanctioned axioms in SafetyLemmas.idr (enforced by scripts/check-trusted-base.sh) * %default total on all Idris2 files * IsUnbreakable: only Ready cartridges pass the proof * Chainguard base images, Containerfile not Dockerfile, Podman not Docker diff --git a/docs/outreach/awesome-list-descriptions.adoc b/docs/outreach/awesome-list-descriptions.adoc index 4409fb4f..e9e03c44 100644 --- a/docs/outreach/awesome-list-descriptions.adoc +++ b/docs/outreach/awesome-list-descriptions.adoc @@ -82,7 +82,7 @@ Repository: https://github.com/joaomilho/awesome-idris (or similar) [source,markdown] ---- -- [boj-server](https://github.com/hyperpolymath/boj-server) - Developer tool catalogue using Idris2 dependent types for ABI definitions. The `IsUnbreakable` proof type gates cartridge activation at compile time. 18 cartridge ABI modules with `%default total`, zero `believe_me`. Zig FFI, zig adapter. +- [boj-server](https://github.com/hyperpolymath/boj-server) - Developer tool catalogue using Idris2 dependent types for ABI definitions. The `IsUnbreakable` proof type gates cartridge activation at compile time. 17 core ABI modules with `%default total`; `believe_me` confined to 4 documented axioms. Zig FFI, zig adapter. ---- ''''' diff --git a/docs/outreach/blog-post-draft.adoc b/docs/outreach/blog-post-draft.adoc index b89615e9..4a9aaa01 100644 --- a/docs/outreach/blog-post-draft.adoc +++ b/docs/outreach/blog-post-draft.adoc @@ -233,8 +233,8 @@ BoJ is Alpha. Grade D on most cartridges. Here’s what’s real: (all mutex-protected) * MCP stdio bridge working (JSON-RPC 2.0, all 53 cartridges as tools) * Umoja federation with real QUIC+UDP networking (22 federation tests) -* Zero `+believe_me+` in production code (Idris2’s escape hatch – we -don’t use it) +* `+believe_me+` (Idris2’s escape hatch) confined to four documented, +property-tested axioms over opaque `+Char+`/`+String+` primitives * Security audit by panic-attack scanner: 1 expected weak point (QUIC 0-RTT replay window, mitigated at app layer), 0 critical vulnerabilities diff --git a/docs/outreach/show-hn-draft.adoc b/docs/outreach/show-hn-draft.adoc index 350fcf7f..65da9c73 100644 --- a/docs/outreach/show-hn-draft.adoc +++ b/docs/outreach/show-hn-draft.adoc @@ -11,9 +11,10 @@ What makes it different: calendar), GitHub/GitLab, databases, containers, security (DNS Shield, container hash monitoring, licence-chain provenance via pmpl-mcp), browsers, and more -* *Formal safety proofs* — every cartridge has an Idris2 ABI module with -dependent types and zero `+believe_me+` postulates. The type system -prevents entire classes of runtime errors +* *Formal safety proofs* — an Idris2 ABI with dependent types and +`%default total`; the only `+believe_me+` uses are four documented axioms +over opaque `+Char+`/`+String+` primitives. The proofs are about the Idris +model, which is not yet linked to the running code * *Zero Python, zero TypeScript* — built with Zig (FFI), Idris2 (proofs), and a AffineScript UI. No npm, no pip, no node_modules * *Glama AAA grade* — Security A, License A, Quality A diff --git a/docs/papers/boj-architecture-paper.adoc b/docs/papers/boj-architecture-paper.adoc index 58367952..ef2d709e 100644 --- a/docs/papers/boj-architecture-paper.adoc +++ b/docs/papers/boj-architecture-paper.adoc @@ -511,9 +511,11 @@ These are industry-standard algorithms, but the scanner correctly flags any cryptographic dependency as requiring ongoing review. The finding is expected and documented. -Notably, the codebase contains zero instances of `+believe_me+` (Idris -2’s escape hatch for admitting unproven propositions). All proofs in the -ABI layer are constructive. +The ABI layer’s use of `+believe_me+` (Idris 2’s escape hatch for +admitting unproven propositions) is confined to four documented axioms in +`+SafetyLemmas.idr+` over the opaque `+Char+`/`+String+` primitives, each +backed by property tests; every other proof is constructive. CI fails on +any other escape hatch or on axiom-count drift. ==== 5.3 Resource Footprint diff --git a/docs/quickstarts/DEV.adoc b/docs/quickstarts/DEV.adoc index dd5f0a0d..a6f62e97 100644 --- a/docs/quickstarts/DEV.adoc +++ b/docs/quickstarts/DEV.adoc @@ -37,7 +37,7 @@ just deps # Verify toolchain just build # Build all Zig FFI layers just test # Run all FFI test suites just typecheck # Type-check all Idris2 ABI files -just verify # Full verification (zero believe_me + typecheck + tests) +just verify # Full verification (trusted-base audit + typecheck + tests) ---- == Project Structure diff --git a/docs/quickstarts/USER.adoc b/docs/quickstarts/USER.adoc index 46f4ce52..49d654ec 100644 --- a/docs/quickstarts/USER.adoc +++ b/docs/quickstarts/USER.adoc @@ -105,7 +105,7 @@ just test == Verification -BoJ requires zero `believe_me` in all Idris2 sources. Run the full verification suite: +BoJ allows no `believe_me` in Idris2 sources except the four documented axioms in `src/abi/Boj/SafetyLemmas.idr`. Run the full verification suite: [source,bash] ---- diff --git a/docs/wikis/Developer-Guide.adoc b/docs/wikis/Developer-Guide.adoc index 31cd1fe1..14b64aea 100644 --- a/docs/wikis/Developer-Guide.adoc +++ b/docs/wikis/Developer-Guide.adoc @@ -25,7 +25,7 @@ Idris2 ABI (formal proofs) --> Zig FFI (native execution) --> Elixir Adapter (ne | *ABI* | Idris2 -| Dependent-type proofs, state machines, `%default total`, zero `believe_me` +| Dependent-type proofs, state machines, `%default total`, `believe_me` only in the 4 core axioms | `src/abi/` (core), `cartridges/*/abi/` | *FFI* @@ -135,7 +135,7 @@ With `just`: just deps # Verify toolchain just build # Build all Zig FFI layers just typecheck # Type-check all Idris2 ABI files -just verify # Full verification (zero believe_me + typecheck + tests) +just verify # Full verification (trusted-base audit + typecheck + tests) ---- == Adding a New Cartridge diff --git a/mcp-bridge/lib/tools.js b/mcp-bridge/lib/tools.js index fb6c9258..247c56c9 100644 --- a/mcp-bridge/lib/tools.js +++ b/mcp-bridge/lib/tools.js @@ -150,7 +150,7 @@ function buildToolList(scope) { required: ["name"], additionalProperties: false, }, - annotations: { title: "Invoke Cartridge", readOnlyHint: false, destructiveHint: false, idempotentHint: false, openWorldHint: true }, + annotations: { title: "Invoke Cartridge", readOnlyHint: false, destructiveHint: true, idempotentHint: false, openWorldHint: true }, outputSchema: passthrough("Raw JSON response from the target cartridge — shape is owned by the downstream cartridge's manifest, so it is not enumerated here."), }); @@ -315,9 +315,9 @@ function buildToolList(scope) { }); tools.push({ name: "boj_browser_read_page", - description: "Extract the visible text content of the active tab. Read-only; no side effects. Concatenates body text, strips scripts/styles, and preserves rough reading order. Returns `{url, title, text, text_length}` with content capped at ~1 MB for context efficiency. Use after navigation has settled to provide page content to the LLM for analysis.", + description: "Extract the visible text content of the active tab without navigating it. Concatenates body text, strips scripts/styles, and preserves rough reading order. Returns `{url, title, text, text_length}` with content capped at ~1 MB for context efficiency. Use after navigation has settled to provide page content to the LLM for analysis.", inputSchema: { type: "object", properties: {}, additionalProperties: false }, - annotations: { title: "Browser Read Page", readOnlyHint: true, destructiveHint: false, idempotentHint: false, openWorldHint: true }, + annotations: { title: "Browser Read Page", readOnlyHint: false, destructiveHint: false, idempotentHint: false, openWorldHint: true }, outputSchema: { type: "object", description: "Extracted visible text of the active tab, capped at ~1 MB.", @@ -332,9 +332,9 @@ function buildToolList(scope) { }); tools.push({ name: "boj_browser_screenshot", - description: "Capture a PNG screenshot of the active tab's current viewport. Read-only; no side effects. Returns base64-encoded image bytes under `{ok:true, image_base64, mime:\"image/png\"}`. Use when text extraction via `boj_browser_read_page` is insufficient, such as for analyzing complex layouts, charts, or visual bugs.", + description: "Capture a PNG screenshot of the active tab's current viewport without navigating it. Returns base64-encoded image bytes under `{ok:true, image_base64, mime:\"image/png\"}`. Use when text extraction via `boj_browser_read_page` is insufficient, such as for analyzing complex layouts, charts, or visual bugs.", inputSchema: { type: "object", properties: {}, additionalProperties: false }, - annotations: { title: "Browser Screenshot", readOnlyHint: true, destructiveHint: false, idempotentHint: false, openWorldHint: true }, + annotations: { title: "Browser Screenshot", readOnlyHint: false, destructiveHint: false, idempotentHint: false, openWorldHint: true }, outputSchema: { type: "object", description: "PNG screenshot of the active tab viewport as base64 image bytes.", @@ -404,7 +404,7 @@ function buildToolList(scope) { { name: "boj_github_search_code", desc: "Search code across GitHub using the Code Search API v2. Read-only; no side effects. Query syntax supports `repo:`, `language:`, `path:`, `symbol:` qualifiers. Returns an object with `total_count` and an `items` array of match results. Rate-limited to 30 requests per minute. Excellent for finding usage patterns or specific symbols across repositories.", props: { query: { type: "string", description: "Code search query, e.g. `repo:hyperpolymath/boj-server \"coord_register\"`. See GitHub's Code Search syntax documentation.", minLength: 1 } }, req: ["query"], ann: { title: "Search GitHub Code", readOnlyHint: true, destructiveHint: false, idempotentHint: true, openWorldHint: true }, out: { type: "object", description: "GitHub code-search results.", properties: { total_count: { type: "number", description: "Total matches." }, items: { type: "array", description: "Match result objects." } }, additionalProperties: true } }, { name: "boj_github_search_issues", desc: "Search issues and pull requests across GitHub. Read-only; no side effects. Query syntax supports `repo:`, `is:issue|pr`, `is:open|closed`, `author:`, `label:`. Returns an object with `total_count` and an `items` array of issues/PRs. Useful for finding existing reports or discussions related to a specific topic.", props: { query: { type: "string", description: "Issues search query, e.g. `repo:foo/bar is:pr is:open label:security`.", minLength: 1 } }, req: ["query"], ann: { title: "Search GitHub Issues", readOnlyHint: true, destructiveHint: false, idempotentHint: true, openWorldHint: true }, out: { type: "object", description: "GitHub issue/PR search results.", properties: { total_count: { type: "number", description: "Total matches." }, items: { type: "array", description: "Issue/PR result objects." } }, additionalProperties: true } }, { name: "boj_github_get_file", desc: "Read a file's contents from a GitHub repository at a specific branch, tag, or commit. Read-only; no side effects. Decodes base64 content automatically for text files. Returns `{path, content, sha, encoding:\"utf-8\"}`. Binary files preserve the raw base64 encoding. Useful for inspecting code or reading configuration files without cloning.", props: { owner: { type: "string", description: "Repo owner login." }, repo: { type: "string", description: "Repo name." }, path: { type: "string", description: "Repo-relative path (no leading slash), e.g. `src/main.js`." }, ref: { type: "string", description: "Branch, tag, or commit SHA. Defaults to the repo's default branch if omitted." } }, req: ["owner", "repo", "path"], ann: { title: "Get GitHub File", readOnlyHint: true, destructiveHint: false, idempotentHint: true, openWorldHint: true }, out: { type: "object", description: "File contents at the requested ref; text decoded from base64, binaries kept as base64.", properties: { path: { type: "string", description: "Repo-relative path." }, content: { type: "string", description: "File contents (decoded UTF-8 or raw base64 for binary)." }, sha: { type: "string", description: "Blob SHA." }, encoding: { type: "string", description: "`utf-8` for text, `base64` for binary." } }, additionalProperties: true } }, - { name: "boj_github_graphql", desc: "Execute an arbitrary GitHub GraphQL v4 query. Can be Read-only or Side-effectful depending on the query (query vs mutation). Use when REST endpoints are insufficient, such as for batching requests, fetching nested fragments, or custom data aggregates. Returns the raw GraphQL response `{data, errors?}`. Requires a valid schema-compliant query string.", props: { query: { type: "string", description: "GraphQL document. Supports `query` and `mutation` operations.", minLength: 1 }, variables: { type: "object", description: "Optional GraphQL variables object, keyed by `$name` references inside the query." } }, req: ["query"], ann: { title: "GitHub GraphQL", readOnlyHint: false, destructiveHint: false, idempotentHint: false, openWorldHint: true }, out: { type: "object", description: "Raw GitHub GraphQL response. Can be a query (read) or a mutation (write) depending on the supplied document.", properties: { data: { type: "object", description: "GraphQL data payload." }, errors: { type: "array", description: "GraphQL errors, present only on failure." } }, additionalProperties: true } }, + { name: "boj_github_graphql", desc: "Execute an arbitrary GitHub GraphQL v4 query. Can be Read-only or Side-effectful depending on the query (query vs mutation). Use when REST endpoints are insufficient, such as for batching requests, fetching nested fragments, or custom data aggregates. Returns the raw GraphQL response `{data, errors?}`. Requires a valid schema-compliant query string.", props: { query: { type: "string", description: "GraphQL document. Supports `query` and `mutation` operations.", minLength: 1 }, variables: { type: "object", description: "Optional GraphQL variables object, keyed by `$name` references inside the query." } }, req: ["query"], ann: { title: "GitHub GraphQL", readOnlyHint: false, destructiveHint: true, idempotentHint: false, openWorldHint: true }, out: { type: "object", description: "Raw GitHub GraphQL response. Can be a query (read) or a mutation (write) depending on the supplied document.", properties: { data: { type: "object", description: "GraphQL data payload." }, errors: { type: "array", description: "GraphQL errors, present only on failure." } }, additionalProperties: true } }, ]; for (const t of ghTools) { tools.push({ name: t.name, description: t.desc, inputSchema: { type: "object", properties: t.props, required: t.req || [], additionalProperties: false }, annotations: t.ann, outputSchema: t.out }); diff --git a/site/index.html b/site/index.html index 5aecf100..901f45d3 100644 --- a/site/index.html +++ b/site/index.html @@ -157,9 +157,19 @@

What BoJ does

Comms

Gmail, Google Calendar, Slack, Discord, Telegram, Matrix

Browser

Headless navigation, screenshots, JS execution

Research / ML

Web search, deep research, HuggingFace models & datasets

-
Verified

Constructive proofs over the catalogue, dispatch, and credential isolation

+ +
+

What is proven, witnessed, and trusted

+

"Proven" here means proven about a model. Each claim sits in one of three bins.

+
+
Proven

An Idris2 model of the safety predicates, catalogue, dispatch and credential isolation, total, with four documented axioms. It does not typecheck at the moment (a duplicate lemma, and a broken CI job); the fix is pending. The model is not yet linked to the running server, and 13 of the runtime checks it binds are not yet implemented.

+
Witnessed

Property tests on the four axioms, coherence tests between advertised and dispatched tools, npm provenance, SLSA level 3 release tarballs, container attestation.

+
Trusted

The JavaScript bridge and Zig FFI themselves, hand-written tool annotations, cloud and forge APIs, compilers, runtimes, the OS, and the AI choosing the right tool.

+
+

Full breakdown in the README

+