Machine-checked governance for the agentic layer of AI — six papers, read in order or any on its own.
Each is mirrored as a signed PDF in the
repository;
for the framework itself, see the legitimacy project page.
The program in one pass: what a machine-checked governance compiler is, what it found when pointed at real agent harnesses, and why the governance layer is the unguarded surface.
The kernel object: a runtime layer plus an explicit bridge contract, inhabited by a concrete instance — a compiler target for the governance layer of AI agents.
No rule rationing scarce permission among an agent's competing requests can be consistent, solidary, and cross-claimant monotone at once — proved in Lean, and any legitimate rule must declare which it gives up.
Capacity and stability bounds: a governance graph stays stable at unbounded capability exactly when its consistency vulnerability is zero; any positive vulnerability gives a finite, computable stability cliff.
Source-walked audits of open agent-harness code, producing finite governance-graph fixtures with machine-checked diagnostic certificates over the extracted models.