[hyperpolymath]

Summary

Adds a Proven / Witnessed / Trusted ladder to the README and site, and corrects safety claims that the code does not back: "zero believe_me" (the enforced budget is 4 sanctioned axioms), "formally verified coordination ABI", and four tool annotations. The ladder also says plainly that the Idris core does not typecheck today, because of a duplicate allTake and a CI job that never reaches Idris. That is tracked in #343, which this PR does not fix.

Type of change

• Documentation
• Small code change: four MCP tool annotation values in mcp-bridge/lib/tools.js

📌 New pins

Head SHA: e747484. No action, lockfile, container or actions.lock pins are added or changed.

Changes

• README.adoc + regenerated README.md: new "What is proven" section with the three-column ladder. The Features and Security bullets are rescoped (it is a safety and dispatch ABI model, not a "coordination ABI"). 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, Justfile comments, .claude/CLAUDE.md: "zero believe_me" and "5 axioms" become 4 sanctioned axioms in SafetyLemmas.idr. Rules for cartridge authors ("your ABI must have zero believe_me") are unchanged.
• PROOF-NEEDS.adoc: the count history now reads 5 → 4 (2026-06-24), broken docs/proof-debt.md links are fixed, and a new "Model-to-code obligations" section covers restoring the proof gate, the 13 unimplemented libbozsafety bindings, and effect-typed manifests.
• verification/proofs/README.adoc: 5 → 4 axioms, and charEqSym is marked as discharged.
• src/abi/Boj/SafeHTTP.idr: a comment only. "Zero believe_me" becomes "none in this module; relies on the 4 SafetyLemmas axioms".
• mcp-bridge/lib/tools.js:
  • boj_browser_read_page and boj_browser_screenshot are now readOnlyHint:false, a conservative label until effect-typed manifests land;
  • boj_github_graphql (accepts mutations) and boj_cartridge_invoke (reaches any cartridge) are now destructiveHint:true.

RSR Quality Checklist

Required

• Tests pass: bun test mcp-bridge/tests/ reported 52 pass, 0 fail.
• Code is formatted: not applicable. The only code change is four boolean literals plus two description strings, in the file's existing style.
• Linter is clean: no new code paths. The repo's pre-commit hooks passed on commit.
• No banned language patterns: no new files in any language.
• No unsafe blocks without // SAFETY: comments: none touched.
• No banned functions: none added. Text that mentions believe_me documents the existing 4 axioms. bash scripts/check-trusted-base.sh reported "OK … 4 sanctioned class-(J) axioms".
• SPDX license headers present: no new files, and existing headers are unchanged.
• No secrets, credentials or .env files included.

As Applicable

• .machine_readable/*.a2ml: deliberately not touched. 0-AI-MANIFEST.a2ml and META.a2ml also say "zero believe_me" and are left for the owner's decision.
• Documentation updated for user-facing changes.
• TOPOLOGY.md: not applicable, no architecture change.
• CHANGELOG: not updated; docs-only, no release.
• New dependencies: none.
• ABI/FFI changes validated: not applicable, no ABI or FFI change (one .idr comment only).

Testing

• bun test mcp-bridge/tests/ reported 52 pass, 0 fail.
• README derivation was reproduced locally with the pinned toolchain (pandoc 3.10, asciidoctor 2.0.26). As a control, it first reproduced the committed README.md on main byte-for-byte after normalisation. Then the regenerated file was committed. readme-vocab-gate.sh (standards@84355587) reported 98.7% at a 98% floor; the base was 98.4%.
• bash scripts/check-trusted-base.sh reported OK with 4 axioms.
• cd src/abi && idris2 --typecheck boj.ipkg fails, and fails the same way on main: allTake is already defined. The .idr change is a comment. See Proof gate: core fails to typecheck (duplicate allTake) and CI typecheck job never runs Idris #343.

Red check deferral

• Idris2 type-check (core + all cartridge ABIs) is expected to be red: this PR touches src/abi/ and verification/, which triggers the job, and the job fails on main too (empty asdf version, duplicate allTake). It is not a required check. Deferred to Proof gate: core fails to typecheck (duplicate allTake) and CI typecheck job never runs Idris #343.
• governance / Workflow security linter is red on main too (duplicate with in abi-drift.yml); not required. Deferred to Three pre-existing red non-required checks on main: Allowlist Preflight (empty GH_TOKEN), Workflow security linter (duplicate with in abi-drift.yml), SonarQube (403) #338.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Ge6k9wanwVdYJWBrnwjPxf

[coderabbitai]

Note

Currently processing new changes in this PR. This may take a few minutes, please wait...

⚙️ Run configuration

• Configuration used: Organization UI
• Review profile: ASSERTIVE
• Plan: Advanced
• Run ID: bffe926f-d2d8-49a5-9fae-e0a9462d4b7e

📥 Commits

Reviewing files that changed from the base of the PR and between d836a63 and e747484.

📒 Files selected for processing (21)

• .claude/CLAUDE.md
• Justfile
• PROOF-NEEDS.adoc
• README.adoc
• README.md
• docs/RSR_OUTLINE.adoc
• docs/developer/README.adoc
• docs/developer/llm-warmup-dev.adoc
• docs/developer/llm-warmup-user.adoc
• docs/outreach/awesome-list-descriptions.adoc
• docs/outreach/blog-post-draft.adoc
• docs/outreach/show-hn-draft.adoc
• docs/papers/boj-architecture-paper.adoc
• docs/quickstarts/DEV.adoc
• docs/quickstarts/USER.adoc
• docs/wikis/Developer-Guide.adoc
• mcp-bridge/lib/tools.js
• site/index.html
• src/abi/Boj/SafeHTTP.idr
• src/abi/README.adoc
• verification/proofs/README.adoc

 ________________________
< EV: Electric Verifier. >
 ------------------------
  \
   \   (\__/)
       (•ㅅ•)
       / 　 づ

✨ Finishing Touches

📝 Generate docstrings

• Commit to this branch
• Create a new PR

• Autopilot · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

---

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}

[github-actions]

🏁 path-claims bench

Commit 55f9c6d

Numbers

path-claims bench  (node v22.23.3)

  scenario                                              iters       ms        ns/op          ops/s
  --------------------------------------------------------------------------------------------------------------
  register: 10 active claims, 3 new paths               50000 iters    105 ms      2.12 µs/op    471.8k ops/s
  register: 100 active claims, 3 new paths              20000 iters    168 ms      8.43 µs/op    118.6k ops/s
  register: 1000 active claims, 3 new paths              5000 iters    535 ms    107.03 µs/op      9.3k ops/s
  register: 100 active claims, 20 new paths              5000 iters    207 ms     41.47 µs/op     24.1k ops/s

  pathsOverlap: deep diverge at segment 4             1000000 iters     88 ms      88.5 ns/op    11.31M ops/s
  pathsOverlap: short prefix match                    1000000 iters     76 ms      76.1 ns/op    13.14M ops/s

  refresh (existing claim)                             100000 iters      8 ms      80.9 ns/op    12.36M ops/s
  list (100 active claims)                              50000 iters    227 ms      4.54 µs/op    220.2k ops/s

  (Bench numbers depend on host; use deltas across commits, not absolute values.)

Host-dependent — compare deltas across commits, not absolute values.

[github-actions]

🔍 Hypatia Security Scan

Findings: 114 issues detected

Severity	Count
🔴 Critical	10
🟠 High	22
🟡 Medium	82

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Job `sonarqube` in build.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/build.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "sonarqube"
  },
  {
    "reason": "Job `triage` in label-triage.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/label-triage.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "triage"
  },
  {
    "reason": "Job `sync` in labels.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/labels.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "sync"
  },
  {
    "reason": "Job `deploy` in pages-deploy.yml has no `timeout-minutes:` declaration. Default is 6 hours — a stuck codeload fetch or runner hang can burn budget. Add `timeout-minutes: 10` (or proportional).",
    "type": "missing_timeout_minutes",
    "file": ".github/workflows/pages-deploy.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "recipe_id": "recipe-add-workflow-timeout-minutes",
    "job": "deploy"
  },
  {
    "reason": "Step uses `peter-evans/repository-dispatch` with `token: ${{ secrets.FARM_DISPATCH_TOKEN }}` but has no `if: secrets.FARM_DISPATCH_TOKEN != ''` gate. On repos where the secret hasn't been propagated the action fails on every push, red-maining the repo. Add the step-level gate (or env+if pattern) so the missing-secret path is a clean skip instead of a red.",
    "type": "secret_action_without_presence_gate",
    "file": ".github/workflows/instant-sync.yml",
    "action": "peter-evans/repository-dispatch",
    "rule_module": "workflow_audit",
    "severity": "high",
    "fix_recipe": "add_secret_presence_gate"
  },
  {
    "reason": "codeql.yml does not list `language: actions` in its matrix, but the repo has workflow files. CodeQL's `actions` language scans workflow YAML for injection and other CI/CD-specific weaknesses — every repo with workflows benefits. Add an entry to `matrix.include` with `language: actions` + `build-mode: none`.",
    "type": "codeql_missing_actions_language",
    "file": ".github/workflows/codeql.yml",
    "action": "flag",
    "rule_module": "workflow_audit",
    "severity": "medium",
    "fix_recipe": "add_codeql_actions_language"
  },
  {
    "line": 39,
    "reason": "job in .github/workflows/labels.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/labels.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 46,
    "reason": "job in .github/workflows/push-email-notify.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/push-email-notify.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 32,
    "reason": "job in .github/workflows/build.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/build.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  },
  {
    "line": 44,
    "reason": "job in .github/workflows/container-publish.yml references `secrets.*` but does not install `step-security/harden-runner` — review outbound-egress monitoring",
    "type": "RE001",
    "file": ".github/workflows/container-publish.yml",
    "action": "report",
    "rule_module": "research_extensions",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence