biject authorizes AI-agent tool calls with machine-checked proofs. A proposed action is compiled to a decidable proposition and decided by the Lean 4 proof kernel in microseconds. Every verdict is Ed25519-signed and appended to a Merkle hash chain you can verify yourself.
biject never reads natural language at runtime. It receives typed parameter values and decides a compiled predicate — so there is nothing in it to argue with, and no wording that changes the answer.
This demo puts the same tool calls past two things side by side: the kernel, and an LLM-as-Judge (representative architecture) — a reasoning-based verdict over full context, re-evaluated per call, which is the pattern shared by most current agentic guardrail systems. It is a measurement, not a pitch. The numbers on screen come from calls made while you watch, and the arithmetic behind every figure is shown on the screen that reports it.
One fixed tool call, submitted ten times unchanged. The kernel returns the same verdict against the same conjecture digest, ten times over. The reasoning-based reviewer is asked the same question ten times — watch whether it answers the same way. Every verdict is shown, including the ones that disagree.
Fifty calls in sequence, with one event added to a rolling window each time. We plot how often each system's verdict matches what the compiled policy actually decides, as the run goes on. Both sides are given the same window contents and the same declared ceiling.
We take the error rate measured in Act 2 — not a rate from a paper — and extrapolate it to a production call volume you choose. The formula is printed on the screen, along with the interval around it.
Open the wall on the projector. Everything runs there, driven from its own keyboard:
→ ← to move between acts, R to run one, ⏎ to reset.
| authorization | Lean 4 kernel proof over declared parameter values |
| comparison | LLM-as-Judge (representative architecture) — measured, never used to authorize |
| audit | Ed25519 signatures over a Merkle hash chain |
| policies | PHARM-PV-001 PHARM-AUD-001 PHARM-BR-001 PHARM-DISP-001 |
| verify yourself | GET /api/audit/verify · GET /api/audit/head |