This is not a flat manual but documentation in four layers, for four readers: who uses it, who wants to understand the idea, who builds it, and who wants to go further. Each layer carries a label saying how long it keeps.
Layer 1 — for the user1What you do with it moves with the code
/aiThe questionpanel vraag
- Type a question and press "ask". The loop computes the address of your question (the same gate as all material), looks in the ledger first and then in the store, and returns exactly one typed output.
/aiThe outputpanel uitvoer
- If your question is exactly the name of an inhabitant (the name bridge), that is the address: derived via "exact name". If the top inhabitant of the image resembles the question little (cosine below 0.32), it is marked weak: in the store, not an answer.
- Derived (green): an inhabitant of the store at the computed address or at an image of it (a truncation), with the derivation: address, image, depth, how many inhabitants the image holds, and the cosine that ranked this one first. With receipt (source) and the address in the net. The claim is stated below it: this is held by the store — nothing more.
- Attested (gold): someone earlier settled an address for this canonical question; you see who, when and the chain hash. The machine proves that the event is in the ledger and that the content is in the store; whether the settlement was right belongs to the human who signed.
- Vacancy (rust): nothing is held at the computed address or its images down to depth 6. Empty is empty; nothing is invented.
- Proposal (blue, dimmed): what the language model says about the sources found, with the addresses it cites. It asserts nothing and is never the answer.
- Below a derived output is settle: enter your name (and the admin key, or later your SWARP registration) and from then on the question carries this address as attested answer — a row in the ledger.
/aiState of affairspanel stand
- At the top of the MAZE.AI page, collapsible: what the system can and cannot do as of the latest booking — so that "done" is never misread again. Can: the net, the loop that never invents (proven), the ledger, the office, the field as instrument, the calibration series. Cannot: think by itself (the proposal comes from an external language model), placement 71–78%, empty ledger, external embeddings, one resonance measure counting as tiebreaker only.
/ai/kantoorThe office registerpanels kantoor-vraag, kantoor-vacatures, kantoor-kast, kantoor-register, kantoor-sleutel
- A register, not a chatbot (design J. Konstapel 20-9, for the notarial profession; Dutch-language UI). Question: one field with area of law; below it answer cards with a fixed anatomy — status bar in fixed colour and wording (ATTESTED "Settled answer" + who, date; DERIVED "From the office cabinet"; VACANCY "Nothing has been settled about this in the cabinet."; PROPOSAL grey, always last: "Proposal by the language model — not an answer."), the content, the provenance line (address, source, receipt, derivation, cos), an amber band on weak placement, the Chain button (canonical question, canon version, hash, ledger row, previous hash), neighbour cells, and Card as PDF (a print of the verified card with chain — no second path).
- Settling as an act: only the role notary/candidate-notary sees the button; a separate confirmation step shows literally what will be recorded (canonical question, address, piece, name, date, key fingerprint) and only the Settle button writes the ledger row — signed with the person's own office key. Two settlements of the same question both remain visible; the latest is operative.
- Vacancies = the work backlog per area of law; "Add piece" opens intake. Cabinet: intake only with a receipt (source file, version, who from the key, date); afterwards the computed address and neighbour cells; an inhabited address reports "this address is inhabited; a new version is a new piece". Register: the ledger searchable by question, person, date; "Check chain" and "Check my signatures" (only the holder of a key can verify its signatures). Key: sign in with the office key (kept in the browser session; the server stores only a fingerprint); admin assigns roles with the admin key.
- Own cabinet first (21-9, from the office test `kantoor-toets.md`): with an office key every question is first matched against all pieces of the own cabinet by similarity (embedding of name + text); a hit from cos 0.45 precedes everything from the shared net (`afleiding.via = "kast"`), below 0.60 with the weak band. Without a key this step does not exist.
- Office cabinet (21-9, open since 27-10): pieces with source
kantoor:…are ordinary residents, findable by anyone (Hans: secrecy hampers the exchange of information). With an office key the own cabinet is searched first (`lus(vraag, { kantoor })`). Text is sent to OpenAI for embedding. - Boundary, on every page: this is not an authentic deed and replaces no legal form. Explanation for the notary (why, what, how; Dutch): /ai/kantoor/uitleg (PDF).
/ai/veldThe field (RAI)panels veld-stand, veld-regio, veld-koppeling, veld-dagen
- RAI as a simulated field beside the loop (definitions by Hans 21-9, `maze/rai/veld.mjs`, plan `maze/rai/plan-veld.md`): one oscillator per inhabited region (address prefix at depth 6) with a region frame (centre, principal direction, sign from the earliest piece); the phase of every piece — a fresh proposal too — is φ = atan2(x·e₂, x·e₁); questions, intakes and settlements pull the region phase; couplings between regions learn at every settlement on resonance r·cos(θ_a − θ_q) and decay daily to the base. The page shows the state (regions, r, couplings, daily logs). Every output of
/api/ai/vraagcarriesveldas advice — the field advises, the gate decides, nothing in the loop changes because of it. Two tests are fixed in advance (shuffle test after 14 daily logs; learning rule after 30 settlements).
/aiThe ledgerpanel grootboek
- All settlements: canonical question, inhabitant, who, when, hash. Append-only and hash-chained; below it the chain check (rows, intact or not, final hash).
Layer 2 — for the thinker2The idea & the rules lasting
A provable AI is not an AI whose every behaviour is proved — Tarski blocks that: there is no total certified meaning relation for open language. It is an AI whose every claim is proved (paper Provable AI, Konstapel 2026, Criterion P). So the loop claims one thing only: this is the content of the certified store at the computed address, reached by the recorded derivation. Never "this is true of the world". Natural language yields proposals; an empty address yields a vacancy; meaning is settled by a human, and that settlement is an event in a chained ledger — checkable as a fact, never as a truth.
Three invariants carry it, machine-checked in Lean 4 against running definitions (maze/lean/MazeAI/Lus.lean): derived ⇒ the pair is in the store; vacancy ⇒ the address is empty; attested ⇒ a ledger row settled this address for this canonical question by a named human on a date, and the content is in the store. Beneath lies the kernel of the address itself: bijection, range, uniqueness, truncation idempotent and prefix-stable — also proved, and differentially tested against the running JavaScript kernel (30,572 addresses, 0 differences).
The MAZE invariants return here as types: the address comes from the content (the same gate for question and material), empty is empty, counters touch no address, and nothing reaches the user outside the loop.
Layer 3 — for the builder3How it works — loop, ledger & API moves with the code
Context under the-maze: maze/ai/lus.mjs (the loop, settling, chain check), canon.mjs, verifier.mjs, route.mjs, pagina.html; table ai_attest (canon_versie, canon_q, vraag, materiaal_id, pad, who, via, date, prev_hash, hash). canon-1: NFKC, lower case, letters/digits/spaces only, single spaces, trimmed, max 400 characters — deterministic, no semantics; every row carries the canon version. The loop: ledger on (canon version, canon_q) → latest row → inhabitant from the store (else the row is skipped and the loop continues); otherwise adresVoorTekst (generation 2) → thuiskomst with minDiepte 6 → top inhabitant by cosine = derived (the image = the deepest inhabited prefix), no inhabitants = vacancy. Settling: hash = sha256(prev ⧺ canon version ⧺ canon_q ⧺ materiaal_id ⧺ pad ⧺ who ⧺ date); prev = last hash or 64 zeros; verifieerKeten walks the whole list (the chain_snoc form from Lean). The proposal comes from the existing question side (gesprek.mjs, gpt-4o) and is attached typed; the model is swappable (DeepSeek, BitNet) without changing the loop.
Whitepaper: /ai/whitepaper, PDF. The maze.ai/1 spec (19-9), what stands. Canon as its own module maze/ai/canon.mjs (canon-1, frozen examples) with determinism test canon-toets.mjs (idempotence, repetition, shape, 5,000 random inputs). Verifier C4 maze/ai/verifier.mjs: a small separate module every output must pass before it leaves — it re-reads store and ledger and checks the three invariants; if it refuses, nothing leaves (500 with reason), never a silent rewrite. One output path (§9): the main page (POST /api/gesprek) also goes through the loop — the conversation is the proposal, the loop output sits above it, both pass the verifier. The single control command (§8d) node maze/ai/controle.mjs: Lean rebuild + axiom report, differential kernel test (30,572 addresses), canon test and — with DATABASE_URL — the production-path test lus-toets.mjs (the real loop on the real store, every output through the verifier, chain check). An empty question is a vacancy with reason. Question side after calibration (20-9, plans 5–11, `uitkomst-honderd*.md`): word sequences of 2–6 words from the question matched exactly against names (plus parenthetical variants and single capitalised words), chosen by cosine to the question; the language model as title proposer (it names a Wikipedia title, the net decides on membership and cosine — via: "voorstel-titel"); and the reverse direction maze_noemt (who mentions whom, from the DBpedia abstracts): for a descriptive question the loop searches among those who mention the anchor (via: "genoemd-door"). Measured on one hundred blind questions: 18 → 71–73, fresh set 76–78; since plan 18 the name bridge searches all sources (including Konstapel's own essays, `konstapel:essay`, 99 pieces with receipts) and knows acronyms (plan 19). Since plan 17 the ring measure R_Q (Maxwell essay 4th ed. §15, region frames from the field, Markley averaging; plan 16d AUC 0.70) decides a tie < 0.05 in cosine between the two top candidates — booked in afleiding.ringmaat. Neighbour cells (§8i): on a derived output the loop returns the neighbours on the image, each with its own address; the main page shows them as cells next to the inhabitant.
Known limits. "Derived" uses the deepest inhabited prefix as image and ranks by cosine; the Lean loop models exact lookup — the verifier therefore checks store membership and address provenance (the inhabitant's address, or the image as prefix), not meaning; the zwak flag (cos < 0.32) says when the top inhabitant resembles the question little. Every row now carries a signature (HMAC-sha256 over the row hash with the key that admitted the settlement, plus that key's fingerprint — handtekening, sleutel_vinger); the chain check verifies it and counts ondertekend. Publicly verifiable (27 Oct): since 27 October the server also signs every new row with Ed25519 (ed_handtekening, ed_vinger), whose public half is at /api/ai/sleutel. Only the key holder can check the HMAC signature; anyone can check the Ed25519 one. Older rows were not rewritten: the signed head (row count + final hash) covers them through the chain. To check without key or database: node maze/ai/verifieer-extern.mjs. Limit: the signature proves the server recorded the row this way, not who sat at the keyboard; for assurance against the server itself, keep a head now and then — a later export must contain it as its beginning. Test ed-toets.mjs (ten planted errors, all red). Personal keys per human do not exist yet (who stays a name next to the key fingerprint); the chain proves order and immutability under the hypothesis that sha256 is collision-free. The store is also proved in Lean as a finite map (MazeAI/Winkel.lean: derived ⇔ in the store, write-once as a theorem). Placement quality on open questions is unmeasured (the twenty-question test is prescribed).
Layer 4 — for the connector4Links, sources & further moves with the code
- MAZE.AImaze.swarp.nl/ai · API · the proofs:
maze/lean/(Trit, Kern1, Brug, Keten, Lus) - theoryJ. Konstapel, Provable AI — A Claim-Bounded Criterion, a Semantic Boundary, and a Machine-Checked Construction (2026); Where Computation Comes From (2026); Tarski 1936; Necula, Proof-Carrying Code (1997); Klein et al., seL4 (2009)
- familythe MAZE (the store, the gate) · the Bank and the Doorgang (the same hash chains) · the Patent Generator
- honestyproved what can be proved (provenance), measured what must be measured (placement), settled what no one can prove (meaning) — each named as such