fix: repair allTake proof break; MPL-2.0 licensing; Markdown README; reconcile counts (125/68/0.4.7) (#256)

## Summary

Three independent fixes — split for review — that lift BoJ's Glama
grades and repair a **real proof break** that was sitting in `main`.

### 1. `fix(abi)` — duplicate `allTake` proof (`daf8129a`)
`src/abi/Boj/SafetyLemmas.idr` defined `allTake` twice (a merge
artifact; both clauses prove the identical proposition, differing only
in implicit-arg order), so the core `boj.ipkg` failed to type-check.
Removed the redundant copy. **Proof gate: `PASS=104 FAIL=1` → `PASS=105
FAIL=0`**; trusted base unchanged (5 sanctioned class-(J) axioms).

### 2. `chore(license,packaging)` — MPL-2.0, Markdown README, npm
hygiene (`04cdf2fa`)
- Restore `MPL-2.0` in `package.json` (the published `0.4.7` is already
MPL; the working-tree `AGPL-3.0-or-later` was a regression) and switch 6
sub-manifests AGPL→MPL (`elixir/mix.exs`, `coord-tui`/`tray`
`Cargo.toml`, three `tools/*` packages). `cartridges/idaptik-admin-mcp`
intentionally left AGPL.
- Rewrite `README.md` as real GitHub-Flavored Markdown — it was AsciiDoc
markup in a `.md` file, which renders garbled on GitHub/npm/Glama.
- Add a `files` whitelist (npm tarball ~10.5 MB → ~0.9 MB); fix the
`main.js` shebang (`deno run` → `node`) so `npx` runs; add
`.gitattributes` linguist overrides so the repo stops being detected as
"Zig".

### 3. `docs(metadata)` — reconcile counts to one source of truth
(`14a43ee6`)
**125 cartridges** (= `cartridge.json` count = live `boj_menu`), **68
tools** (45 `boj_*` + 23 `coord_*`), **v0.4.7**. Completed the smithery
`tools:` table 18 → 68 (generated from the live `tools/list`); replaced
the inflated "1041 Tools" with the honest 68; synced versions. Dated
`2026-04-30` measurement snapshots, ADRs, and code line-counts were left
untouched on purpose.

## Verification
- `scripts/check-trusted-base.sh` ✓ (5 axioms) · `idris2 --check
Boj/SafetyLemmas.idr` ✓
- `scripts/typecheck-proofs.sh` → `PASS=105 FAIL=0`
- JS: dispatch 15/15, http_transport 26/26, path_claims 11/11 ·
`boot_smoke` ✓ on node/bun/deno (68 tools)

## Notes
- Docs are tagged `MPL-2.0` to satisfy the repo's current single-licence
pre-commit hook. Moving prose to **CC-BY-SA-4.0** needs a hook +
`.reuse/dep5` change (tracked as a follow-up).
- A pre-existing, unrelated `elixir/boj-rest.service` working-tree
change was deliberately excluded from these commits.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.gitattributes

@@ -58,3 +58,12 @@ Containerfile  text eol=lf
 # Lock files
 Cargo.lock  text eol=lf -diff
 flake.lock  text eol=lf -diff
+
+# GitHub Linguist — surface the JS/Deno MCP bridge (mcp-bridge/) as the
+# primary language instead of the bulky Zig FFI / generated cartridge code.
+cartridges/**   linguist-vendored
+ffi/**          linguist-vendored
+generated/**    linguist-generated
+*.adoc          linguist-documentation
+docs/**         linguist-documentation
+proofs/**       linguist-documentation

.github/settings.yml

@@ -11,7 +11,7 @@
 
 repository:
   name: "boj-server"
-  description: "BoJ (Bundle of Joy) — unified MCP server consolidating GitHub, GitLab, Cloudflare, browser automation, and 50+ open-source cartridges"
+  description: "BoJ (Bundle of Joy) — unified MCP server consolidating GitHub, GitLab, Cloudflare, browser automation, and 125 open-source cartridges"
   homepage: "https://github.com/hyperpolymath/boj-server"
   private: false
   has_issues: true

.machine_readable/contractiles/intend/Intentfile.a2ml

@@ -18,7 +18,7 @@ LLM/SLM agents: understand what this repo IS and IS NOT before acting.
 BoJ (Bundle of Joy) is a unified MCP server that consolidates all hyperpolymath
 tooling into a single endpoint. It provides Claude Code integration for GitHub,
 GitLab, Cloudflare, Vercel, Verpex, Gmail, Calendar, browser automation, research,
-ML, and 50+ open-source cartridges. It implements a three-class architecture:
+ML, and 125 open-source cartridges. It implements a three-class architecture:
 - Class 1 (Simple Track): zero-infrastructure CLI/curl workflows
 - Class 2 (Orchestrator Track): HMAC-SHA256 webhooks and real-time MQTT/WS
 - Class 3 (Multiplier Track): Elixir/BEAM mass concurrency

CITATION.cff

@@ -18,7 +18,7 @@ abstract: >-
   gateway. Each cartridge — covering databases, container runtimes, git forges,
   Kubernetes, observability, secrets, IaC, cloud providers, and multi-instance
   AI coordination — is a formally verified Idris2 ABI + Zig FFI + Deno/JS
-  adapter triple. The server exposes 115 cartridges through a unified stdio
+  adapter triple. The server exposes 125 cartridges through a unified stdio
   MCP surface plus a local REST API on port 7700. A local-coord-mcp cartridge
   provides loopback peer discovery, typed envelopes, claim/heartbeat/watchdog,
   and master/journeyman/apprentice supervision for multi-agent AI workflows.
@@ -34,5 +34,5 @@ keywords:
   - multi-agent
   - ai-coordination
 license: MPL-2.0
-version: 0.4.6
+version: 0.4.7
 date-released: "2026-04-27"

README.md

@@ -1,9 +1,9 @@
 <!--
-SPDX-License-Identifier: CC-BY-SA-4.0
+SPDX-License-Identifier: MPL-2.0
 SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -->
 
-[![OpenSSF Best Practices](https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=opensourcesecurity)](https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/boj-server) [![OpenSSF Scorecard](https://api.scorecard.dev/projects/github.com/hyperpolymath/boj-server/badge)](https://scorecard.dev/viewer/?uri=github.com/hyperpolymath/boj-server) [![License: MPL-2.0](https://img.shields.io/badge/License-MPL_2.0--3.0--or--later-blue.svg)](LICENSE)
+[![OpenSSF Best Practices](https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=opensourcesecurity)](https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/boj-server) [![OpenSSF Scorecard](https://api.scorecard.dev/projects/github.com/hyperpolymath/boj-server/badge)](https://scorecard.dev/viewer/?uri=github.com/hyperpolymath/boj-server) [![License: MPL-2.0](https://img.shields.io/badge/License-MPL_2.0-blue.svg)](LICENSE)
 [![Glama MCP Server](https://glama.ai/mcp/servers/hyperpolymath/boj-server/badge)](https://glama.ai/mcp/servers/hyperpolymath/boj-server) [![Green Hosting](https://api.thegreenwebfoundation.org/greencheckimage/boj-server.net)](https://www.thegreenwebfoundation.org/green-web-check/?url=boj-server.net) [![Software Heritage](https://archive.softwareheritage.org/badge/origin/https://github.com/hyperpolymath/boj-server/)](https://archive.softwareheritage.org/browse/origin/?origin_url=https://github.com/hyperpolymath/boj-server)
 
 BoJ (Bundle of Joy) is a unified MCP server that consolidates all

ai-plugin.json

@@ -2,8 +2,8 @@
   "schema_version": "v1",
   "name_for_human": "Bundle of Joy Server",
   "name_for_model": "boj_server",
-  "description_for_human": "Cartridge-based DevOps toolkit with 115 formally verified domain cartridges spanning database, cloud, git, Kubernetes, containers, observability, secrets, IaC, ML, browser automation, communications, and research.",
-  "description_for_model": "A cartridge-based MCP server exposing 115 DevOps domain cartridges via a unified REST API. Each cartridge has a formally verified Idris2 ABI, Zig FFI bridge, and Deno/JS adapter. Domains include: database (VeriSimDB, PostgreSQL, Redis, DuckDB, MongoDB, Neo4j, ClickHouse, Turso, Supabase, Neon, ArangoDB), cloud providers (AWS, GCP, Cloudflare, Vercel, Verpex, DigitalOcean, Hetzner, Fly.io, Railway, Render, Linode), git forges (GitHub, GitLab), Kubernetes, containers, observability, secrets/vault, IaC, ML/AI (HuggingFace), browser automation (Firefox), communications (Gmail, Calendar), queues, SSG, research (academic papers), and language tooling. Use boj_menu to discover available cartridges, boj_cartridge_info to inspect a cartridge, and boj_cartridge_invoke to call operations.",
+  "description_for_human": "Cartridge-based DevOps toolkit with 125 formally verified domain cartridges spanning database, cloud, git, Kubernetes, containers, observability, secrets, IaC, ML, browser automation, communications, and research.",
+  "description_for_model": "A cartridge-based MCP server exposing 125 DevOps domain cartridges via a unified REST API. Each cartridge has a formally verified Idris2 ABI, Zig FFI bridge, and Deno/JS adapter. Domains include: database (VeriSimDB, PostgreSQL, Redis, DuckDB, MongoDB, Neo4j, ClickHouse, Turso, Supabase, Neon, ArangoDB), cloud providers (AWS, GCP, Cloudflare, Vercel, Verpex, DigitalOcean, Hetzner, Fly.io, Railway, Render, Linode), git forges (GitHub, GitLab), Kubernetes, containers, observability, secrets/vault, IaC, ML/AI (HuggingFace), browser automation (Firefox), communications (Gmail, Calendar), queues, SSG, research (academic papers), and language tooling. Use boj_menu to discover available cartridges, boj_cartridge_info to inspect a cartridge, and boj_cartridge_invoke to call operations.",
   "auth": {
     "type": "none"
   },

coord-tui/Cargo.toml

@@ -6,7 +6,7 @@ version = "0.1.0"
 edition = "2021"
 authors = ["Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"]
 description = "Rapid-setup TUI for BoJ local-coord-mcp (AI multi-instance coordination)"
-license = "AGPL-3.0-or-later"
+license = "MPL-2.0"
 
 # Architecture note: pure functions (state transitions, key dispatch) are
 # deliberately isolated so SPARK/Ada formal modules can replace them later

docs/EXPLAINME.adoc

@@ -19,7 +19,7 @@ This is the Model-Controller-Processor pattern: cartridges are pluggable service
 
 **Location**: `elixir/lib/boj_rest/catalog.ex` (Elixir GenServer cartridge discovery and initialization)
 
-**How verified**: `BojRest.Catalog` scans `cartridges/*/cartridge.json` at startup, reads tool schemas from each, and stores them in an ETS table. It validates `name`, `version`, `tools` required fields and prevents duplicate names. 115 cartridges are auto-discovered. This enables the "unified endpoint" claim: a single REST server exposes the union of all cartridges' tools without hardcoding each one.
+**How verified**: `BojRest.Catalog` scans `cartridges/*/cartridge.json` at startup, reads tool schemas from each, and stores them in an ETS table. It validates `name`, `version`, `tools` required fields and prevents duplicate names. 125 cartridges are auto-discovered. This enables the "unified endpoint" claim: a single REST server exposes the union of all cartridges' tools without hardcoding each one.
 
 **Caveat**: Auto-discovery is runtime dynamic; there is no compile-time verification that all cartridge schemas are valid JSON Schema. A malformed `cartridge.json` is silently skipped at startup. The authoritative manifest format is Nickel (closed decision `boj-cartridge-manifest-format-dd.md`); migration from JSON is future work.
 
@@ -42,15 +42,15 @@ This is the Model-Controller-Processor pattern: cartridges are pluggable service
 | gossamer, burble, ephapax, hypatia, verisimdb, typed-wasm — universal ABI/FFI pattern across the estate
 
 | *Pluggable cartridge architecture*
-| 115 cartridge directories (`cartridges/*/`), each with `abi/`, `ffi/`, `mod.js` structure; auto-discovered at startup via manifest scan
+| 125 cartridge directories (`cartridges/*/`), each with `abi/`, `ffi/`, `mod.js` structure; auto-discovered at startup via manifest scan
 | echidna (prover orchestration as cartridges), hypatia (rule composition), gitbot-fleet (bot cartridges per service)
 
 | *PanLL ReScript workspace layer*
 | `panll/` — ReScript/TEA panel framework, autowiring constraint solver, 108 panels for UI
 | idaptik (game UI panels), gossamer-powered SPAs, PanLL monorepo panels estate-wide
 
 | *panic-attack security gate*
-| Pre-commit `panic-attack assail` enforces PA001-PA025 across all 115 cartridges; security module tests cover injection, unicode bypass, SSRF
+| Pre-commit `panic-attack assail` enforces PA001-PA025 across all 125 cartridges; security module tests cover injection, unicode bypass, SSRF
 | Every RSR repo in the estate; panicbot wraps it in CI
 
 | *Elixir/BEAM + Deno runtime*
@@ -70,7 +70,7 @@ This is the Model-Controller-Processor pattern: cartridges are pluggable service
 | `elixir/lib/boj_rest/js_worker.ex` | GenServer wrapping a single Deno port; newline-delimited JSON protocol
 | `elixir/lib/boj_rest/node_key.ex` | X25519 keypair persistence; ChaCha20-Poly1305 credential decryption
 | `elixir/priv/js_pool_worker.js` | Deno-side pool worker; module cache, env isolation per request
-| `cartridges/*/` | 115 cartridge directories, each with abi/, ffi/, mod.js structure
+| `cartridges/*/` | 125 cartridge directories, each with abi/, ffi/, mod.js structure
 | `src/abi/Boj/` | Idris2 ABI definitions (Protocol, Domain, Catalogue, Safety, etc.)
 | `panll/` | ReScript/TEA panel framework for UI workspace layer
 |===

docs/developer/llm-warmup-dev.adoc

@@ -83,7 +83,7 @@ elixir/                     Elixir/BEAM REST server
   test/                     50 ExUnit tests (catalog, router, crypto, JS dispatch)
   config/                   config.exs / test.exs
 
-cartridges/                 115 cartridge directories
+cartridges/                 125 cartridge directories
   database-mcp/             Example cartridge
     abi/database-mcp.ipkg   Idris2 ABI
     abi/Database/Mcp.idr    Idris2 source
@@ -134,7 +134,7 @@ panll/src/                  PanLL panel (ReScript/TEA)
 ----
 just build            # Build all Zig FFI layers (catalogue + cartridges)
 just build-release    # Optimized build (-Doptimize=ReleaseFast)
-just run              # Start Elixir/BEAM server (REST 7700, auto-discovers 115 cartridges)
+just run              # Start Elixir/BEAM server (REST 7700, auto-discovers 125 cartridges)
 just serve            # Server + Cloudflare tunnel
 just test             # Elixir ExUnit test suite (mix test)
 just test-smoke       # Quick: typecheck core ABI + ExUnit smoke
@@ -229,7 +229,7 @@ POST /cartridge/{name}/invoke: { "tool": "...", "args": {...}, "credential_envel
 
 == Cartridge Matrix
 
-115 cartridges organized in a 2D matrix (Protocol x Domain).
+125 cartridges organized in a 2D matrix (Protocol x Domain).
 Each has: `abi/` (Idris2), `ffi/` (Zig), `mod.js` (Deno adapter).
 View status: `just matrix`
 

docs/developer/llm-warmup-user.adoc

@@ -83,7 +83,7 @@ and many more.
 | Elixir REST server (Catalog, Router, JsWorkerPool)
 
 | `cartridges/`
-| 115 cartridge directories
+| 125 cartridge directories
 
 |===