How we build.
And why the seven properties hold.
We don't test the risk out of code. We prove the math first — in Lean 4, before a line is written — then compile a sealed runtime that writes a Decision Receipt your auditor can verify on a clean machine, without us.
Everyone else starts with code, then tries to test the risk out of it. We start with the math.
Write the formal calculus — the equations and operators the system must obey — then decompose it into lemmas.
The Lean 4 kernel proves each lemma. Pass or fail, no override. No code exists until every lemma holds.
Derive runtime invariants from the proven lemmas, verify them deterministically, then extract the sealed runtime.
Three gates. No code before the math. Every line that ships came through this.
Intent enters as plain language. A sealed, signed, machine-checkable runtime comes out the other end. The funnel narrows from many proofs to one runtime — and nothing crosses a gate it hasn't earned.
Define
Turn intent into a formal specification — what the system must do, must never do, and answers to. Signed on paper before anything runs.
Calculus
Write the math. Equations, operators, and a formal description of the behavior the specification demands — not prose, not pseudocode.
Lemmas
Decompose the calculus into compositional proof obligations. Each lemma is a discrete claim that must be established on its own.
Prove
The Lean 4 kernel establishes each lemma. Pass or fail. No override, no partial credit. What does not prove out does not advance.
Invariants
Derive the runtime contract from the proven lemmas. An invariant exists only because a lemma backs it — no proof, no invariant, never the other way around.
Notebook
Deterministic verification of every invariant. Same inputs, same outputs, every time — recorded so the result can be reproduced exactly.
Extract
Compile the closed proofs into a sealed runtime plus its math contract. The code is correct by construction — it carries the proofs that admitted it, not a test suite that hopes to catch what it missed.
Every governed call writes one of these.
The pipeline ends in a sealed runtime that emits a signed Decision Receipt for every governed call. Inputs, invariants, decision, signature — in one document your auditor can verify on a clean machine without us. Here is what one looks like.
§ Call
§ Invariants evaluated
§ Decision
§ Signature
// receipt_2026-04-30T14:22:08Z.json — raw manifest { "receipt_id": "rcpt_01HX8K2Z9Q4N3R7", "issued_at": "2026-04-30T14:22:08Z", "schema": "smarthaus.receipt/v1", "caller": { "service": "refund-service", "tenant": "acme-corp", "runtime": "ucp@a3f2b1c / said-runtime@7d4e9f2 / mae@b1c8e04" }, "subject": { "order_id": "SO-4419822", "rule": "refund-policy@v9" }, "invariants": [ { "id": "I-01", "name": "refund_le_charge", "result": "pass" }, { "id": "I-02", "name": "within_90d_window", "result": "pass" }, { "id": "I-03", "name": "no_duplicate_refund", "result": "pass" }, { "id": "I-04", "name": "pii_not_leaked", "result": "pass" }, { "id": "I-05", "name": "within_manager_discretion", "result": "pass" } ], "decision": { "allowed": true, "amount": 184.50, "currency": "USD", "selection_hash": "sha256:c7a1…4b8e" }, "signature": { "key_id": "acme-corp-prod-2026", "algo": "ed25519", "hash": "sha256:7a3f…e91c", "sig": "3045…6bf2" } }
§ Replay run · 2026-05-18 09:14 UTC
// replaying rcpt_01HX8K2Z9Q4N3R7 // loading manifest … ok // verifying signature … ok (Ed25519, customer key acme-corp-prod-2026) // resolving runtime … ucp@a3f2b1c / said-runtime@7d4e9f2 / mae@b1c8e04 // loading rule snapshot refund-policy@v9 … ok → re-evaluating I-01 (refund_le_charge) ............... pass → re-evaluating I-02 (within_90d_window) .............. pass → re-evaluating I-03 (no_duplicate_refund) ............ pass → re-evaluating I-04 (pii_not_leaked) .................. pass → re-evaluating I-05 (within_manager_discretion) ...... pass // computing selection hash … sha256:c7a1…4b8e // compared to receipt selection_hash … MATCH REPLAY: byte-identical selection. Receipt verified.
§ What this means
The system applied a named rule, evaluated explicit invariants, and the decision was allowed because every invariant held. Human-readable. Auditor-readable. Board-readable.
The runtime, rule snapshot, invariant set, decision, and signature are captured in a single signed document. Nothing about the call is reconstructible from memory — it is recorded.
Months later, on a clean machine, with no contact with SMARTHAUS, your auditor re-runs the manifest and gets the same selection bytes. The system’s behavior is replayable as a property, not a promise.
Seven properties of Mathematically Governed AI.
By construction. Not by attestation.
These are the seven things every Decision Receipt your runtime emits is signed for. They are the architecture, not a deliverable bolted on at the end.
Same inputs, same outputs, every time.
Every decision links to the rule that admitted it.
The why ships with the answer.
Your auditor verifies on a clean machine, without us.
Any past decision re-runs, byte-identical.
Every claim is falsifiable; no claim is asserted.
Anyone on the open-source toolchain can re-verify.
One proof object. Five readers, each for their own reason.
Each asks a different question. Each gets the same answer — the Decision Receipt above, verified for themselves.
The CIO’s risk team
“What’s the proof authority, and what happens when a proof reopens?”
Lean 4 is the authority. A reopened proof blocks the affected runtime from promoting — no override.
The auditor
“Show me this exact decision, and why.”
A signed Decision Receipt — the rules that fired, the data acted on — replayable on a clean machine, by them, without us.
The regulator
“Show me the controls. Not the policy. The controls.”
Controls built into the code, machine-checkable, reproducible without the vendor in the room.
The board
“How do we know our AI won’t blow up in our faces?”
A per-decision proof object behind every governed call. Defensible without depending on hope.
The court
“Reproduce the decision. On your toolchain. With the customer’s own keys.”
A proof object that re-derives independently — without us in the room, without depending on our testimony.