Projects / legitimacy

legitimacy

Machine-checked coherence for the rules that govern AI agents.

github.com/abenenson/legitimacy ↗

An AI agent is constantly making decisions that aren't about any single output: which tool call runs, what gets written to memory, when something is escalated to a human, which of several competing requests gets the one scarce review slot. That is a governance layer — an institution deciding who gets what authority — and today it is mostly unverified scripts. The usual answer, “AI governance,” checks whether each action is allowed; legitimacy asks a prior question about the rule doing the checking: is it even coherent? On exactly these surfaces, some coherence turns out to be provably impossible — worth knowing before you trust the rule.

The idea

Legitimacy treats an agent's rule layer as an institution — something that allocates authority among competing claims — and asks whether it does so coherently. Two results, both machine-checked in Lean 4:

An impossibility
On the surfaces where a rule rations something scarce among competing requests, no rule can satisfy every reasonable fairness guarantee at once. So a legitimate rule can't quietly hold all of them — it has to declare which one it gives up, bound the sacrifice, and say how it is monitored.
A kernel
A compiled object that carries that declaration plus five checkable obligations: verdicts come with witnesses, decision-relevant state survives audit, authorized supervisors can intervene, locally-safe steps stay safe when composed, and the rule actually governs something. A governance rule you can inspect instead of trust.

Papers

The Legitimacy v1.0.0 set — six papers, readable on this site or as signed PDFs in the repository.

Paper 1 — What the Legitimacy Compiler Found
Paper 2 — Semantic Legitimacy Kernels
Paper 3 — A Verified Impossibility Theorem for Peer-Relative Governance
Paper 4 — Which Governance Structures Survive Unbounded Capability?
Paper 5 — Structural Audits of AI Safety Mechanisms
Paper 6 — The Legitimacy Program in Context

The artifact

legitimacy
Rust + Lean 4 · sorry-free
A Rust crate extracts governance graphs from real agent-harness source and audits them against the kernel obligations, backed by a Lean 4 / Mathlib development with zero sorry, admit, or first-party axiom under the verification gate. The diagnostic bites on real code: under the repository's declared extraction convention, the committed OpenAI Codex and Claude Agent SDK models each expose specific monotonicity failures — results about the extracted graph models, not behavioral verdicts on the live products. Source-to-graph extraction is heuristic and empirical, a stated trusted-base boundary, so reviewers can target attacks at the right layer. Orthogonal to gateway products — they enforce; this audits.

Current state

v1.0.0 · public

Read the source and verification instructions, or download the signed release and paper artifacts. Development continues in a private upstream repository; accepted public contributions are reviewed and integrated through the curated release process.