Trust boundary
What is proven,
What is proven,
and how to check it
The point of the proofs is not a badge. It is that a stranger running the smallest possible check learns the truth about a whole history — and a server that lies is caught. This page draws the honest line between what NULLIUS enforces in running code and what a full deployment proves in Lean and carries through a STARK on seL4.
This is a working system. The capability kernel is real and runs. The formal-methods and microkernel layers are represented with matching structure and named honestly. Nothing here claims a proof it does not have. Take nobody's word for it — including ours.
The two columns
| Guarantee | Enforced here, in running code | In a full deployment |
|---|---|---|
| A · Authority | Every turn carries a real ed25519 signature; every capability is an HMAC tag chain the kernel replays. Forge or amplify one → refused. Breakable in the playground. | authority_guarantee, 19 axiom pins; ed25519 + HMAC + Poseidon2-CR cap-root openings. |
| B · Conservation | Value only moves. Mints are issuer moves from a well cell that goes negative, so per-asset Σ = 0 on every reachable state. | conservation_guarantee, 23 pins; a kernel theorem over integer arithmetic. |
| C · Integrity | Each receipt binds a SHA-256 commitment to the whole post-state. Edit any field and it no longer opens. The explorer flags it. | integrity_guarantee, 24 pins; Poseidon2-permutation collision-resistance. |
| D · Freshness | A per-actor nullifier set: a spent nonce cannot replay. No double-spend. | freshness_guarantee, 12 pins; Poseidon2-CR nullifier tree + PostGST at finality. |
| E · Unfoolability | A light client re-checks the hash chain + signatures + commitments (verifyHistory()), re-executing nothing. It catches the pale ghost. | unfoolability_guarantee, 22 pins; FRI/STARK recursion soundness + Poseidon2-CR + ed25519. |
Check it yourself
Everything the light client does is a function you can run. There is no trusted "verified" flag — the badge is computed from the receipts.
# the whole kernel, proved out end to end (13 checks)
node kernel/selftest.mjs
# ask the node what produces its state — it names the one executor
curl -s nulliussol.xyz/status | grep state_producer
# pull the chain and re-verify it, trusting no server
curl -s nulliussol.xyz/api/verifyThe honest seam. Three things a full deployment has that NULLIUS represents rather than reproduces: (1) the guarantees are machine-checked in Lean, pinned to the kernel's three axioms — here they are enforced by cryptographic code you can run and break; (2) a real on-device STARK proves each turn and rejects a tampered proof — here the recursive fold is stood in for by a hash chain with the same binding property; (3) the executor runs as a protection domain on the seL4 microkernel — here it runs as an ES module in Node and your browser. The structure is faithful; the trust base is stated, not hidden.