Architecture

Architecture

Authoritative source: docs/architecture/README.adoc and TOPOLOGY.md. This page is an orientation map.

Four layers, four languages

MCP client (Claude Code, …)
      │  JSON-RPC over stdio
      ▼
mcp-bridge/        JavaScript — zero deps, runs on Node/Deno/Bun
      │  HTTP
      ▼
elixir/            Elixir/BEAM — REST backend on 127.0.0.1:7700
      │  C ABI (via boj-invoke)
      ▼
ffi/zig/           Zig — catalogue, loader, federation, cartridge shim
      ▲
      │  generated header, checked against
src/abi/           Idris2 — the formally verified contract

Each layer is chosen for one property: JavaScript for reach (every MCP client can run it), BEAM for supervision and concurrency, Zig for a stable C ABI, Idris2 for proofs that hold at compile time.

The cartridge contract

A cartridge is a pluggable capability. The contract is ADR-0006's five symbols:

boj_cartridge_init  deinit  name  version  invoke

invoke returns one of seven frozen return codes. The shared implementation of the convention lives in cartridge_shim.zig, which is vendored byte-identically into every cartridge in the registry and enforced there by a drift gate.

Cartridges themselves live in boj-server-cartridges. Each has an Idris2 abi/, a Zig ffi/, and a loopback adapter/.

What the proofs actually cover

src/abi/ carries the catalogue, protocol, credential-isolation and safe-HTTP contracts, with an IsUnbreakable gate on mounting. The trusted base is deliberately tiny: four sanctioned believe_me axioms, all in SafetyLemmas.idr, all tagged, and counted by a CI gate that fails if the number changes.

Current, measured position: PROOF-NEEDS.md and docs/proof-debt.md.

Where it is honest about itself

• DEBT.md — the technical-debt register, with a reproducing command per item
• docs/READINESS.adoc — component readiness grades
• §Number transparency in the README — what the headline count counts