Legitimacy — Checkable Rules for AI Agents

As AI systems become more capable, alignment increasingly concerns the organization of power. An agent that allocates resources, delegates work, or determines what another agent may do is exercising authority. When agents act together, the consequences depend on how their decisions interact and on the rules that give those decisions force.

Institutional design offers a way to think about this problem. Cooperation within a group can coexist with disregard for people outside it. Individually reasonable decisions can produce an unacceptable collective outcome. Rules that work under ordinary conditions can become vulnerable as participants gain the ability to exploit them. Trustworthy autonomy requires ways to justify decisions, examine consequences, resolve competing claims, and preserve the ability to change course.

Legitimacy studies the rules that could make such autonomy possible. It brings together social choice, formal verification, and models of strategic behavior to ask how governance can remain coherent and correctable as capabilities grow toward superintelligence. Lean proofs and executable Rust experiments make parts of that question precise: which guarantees can coexist, what evidence a governing rule must supply, and how useful action can survive the constraints needed for safety.

See the problem and a repair

A policy forbids publishing both fragments of a protected record. Two agents are each allowed to publish their own fragment. Judged separately, both requests pass. Together, their deliveries violate the policy.

The composition experiment makes this failure concrete. A guard remembers what has already become public and blocks the second disclosure, while still allowing delivery to a private vault or publication of a harmless summary. The forbidden outcome stays the same; useful work remains possible.

Explore the seven outcomes in your browser →
No installation. Inspect recorded deliveries, compare the repair, and change selected evidence to see how the checker responds.

This is a sequential experiment with two supplied identities and synthetic data; it runs no language model. The browser presents captured examples and recomputes finite checks. The separate reproduction guide covers execution, signed receipts, and the Lean proofs of the repair for every finite request sequence in the model. It is not a claim to prevent arbitrary production incidents.

The broader research

Which guarantees can coexist?

For the specified class of symmetric, scarce, coupled allocation rules, consistency, solidarity, and cross-claimant monotonicity cannot all hold. The wider theorem includes the median rule; separating examples show why its conclusion is a choice of sacrifice, not the failure of one fixed guarantee. The governance task is to declare and examine that tradeoff, rather than assume it away.

What must a governing rule earn?

A semantic legitimacy kernel is a mathematical specification connecting a rule to evidence about its decisions, observations, supervisory operations, and interactions with other rules. Its obligations include preserving safety under composition and permitting useful action. Current constructions establish changing-state correction and a real causal handoff in separate examples; a general deployed kernel combining them remains a research objective.

What happens as capability grows?

The capacity and stability results relate a modeled rule's vulnerability to changes in its governing structure to a finite stability limit as capability increases. These are conditional mathematical results with explicit carrier and scaling assumptions, not an empirical forecast of when an AI system becomes uncontrollable.

What can an engineer inspect?

Rust tools extract and audit governance graphs, while committed harness models connect specific diagnoses to Lean-checked results. Fresh extraction is diagnostic evidence; it does not automatically inherit the fixture proofs. Source interpretation has execution-based tests, and the trust-chain map distinguishes proved, tested, and open connections.

Follow the evidence

Start with the five-minute evidence map for what is proved, executed, or still open. The formal overview follows the argument to named declarations, and the module map locates the code. The research comparison distinguishes the contribution from prior work.

The six current manuscripts cover the program, kernel, impossibility theorem, stability bounds, structural audits, and related research. The original v1.0.0 paper archive remains readable here; consult the repository for subsequent revisions.

Get the release

v1.1.1 · public Rust + Lean 4

The signed v1.1.1 release includes the composition experiment and an offline Linux x86_64 bundle. Source and verification instructions are public, with automatic verification on GitHub. The proof gate checks for zero sorry, admit, or first-party axiom; the repository states the remaining model, toolchain, and execution assumptions.