Research Papers

The Three Papers

Programmable Sovereignty

Full title: Programmable Sovereignty: Lean-Attestable Constitutions Over Capability-Bounded Federated Receipts. A polity is a triple (T, C, K): a closed receipt-admission scope T, a Merkle-rooted citizenship roster C, and a constitution K expressed as a finite list of predicates. Institutional authority reduces to four decidable operations on the triple: admission against the receipt scope, attenuation within the roster, bilateral treaty intersection between two constitutions, and amendment refinement within one. Each operation is checked by Rust at the kernel boundary, attested by a named Lean theorem, and signed into a canonical receipt admitted only when constitution and scope both accept.

Lean theorems

Four theorems are proved in formal/lean4/Chio/Chio/Treaty/Intersection.lean. The first two state the main admission properties. The last two connect amendment enactment to a refinement witness in the typed runtime path.

The supplementary package under docs/papers/programmable-sovereignty/supplementary/ includes a self-contained lean-source.tar.gz that compiles all four, plus proof-manifest.toml and theorem-inventory.json naming each declaration and its #print axioms footprint. The build succeeds without sorry and without any project-local axiom.

Runtime and closure

The treaty module crates/kernel/chio-runtime-core/src/treaty.rs implements the runtime checks associated with treaty_admission_iff_predicate_intersection. validate_treaty_scope rejects unsupported schemas, invalid validity windows, missing or duplicate participants, and manifest-hash mismatches; a treaty whose governance ladder hash is unequal to the canonical hash of the manifest fails as a schema-and-predicate check. compute_ladder_intersection then builds the joint action-class table. The pre-dispatch admission hook RuntimeAdmissionHook in crates/kernel/chio-runtime-core/src/admission_hook.rs permits a non-Chio request only when no Chio context is present, denies malformed treaty context, refuses request-borne trust roots and signing keys, and releases reserved continuation state on denial or abort so a replayed continuation is denied.

The three-vendor example is generated by examples/chio-3vendor/src/main.rs. The buyer owns the verifier context; a vendor receipt is imported not when it binds treaty scope, ladder intersection, continuation, lineage, bilateral invocation, and strict DSSE evidence to one canonical subject digest. Each run emits signed positive records (admitted vendor-to-vendor actions) and signed negative records (denied paths) in the same schema. A downstream reviewer can replay the admissions and denials without vendor-internal access. An integration gate reruns the example when a bound component changes.

Evaluation

Each reported number is produced by a script under docs/papers/programmable-sovereignty/bench/; withheld rows are marked rather than estimated. The baseline machine is an Apple M1 Max (10 cores, 32 GB). Four paths are exercised.

Latencies are machine-local and regenerated on every run; the scripts write results under bench/results/ beside the raw log. The dispatch harness redirects CARGO_TARGET_DIR into a temporary directory so measurement does not mutate the source tree.

Tool Calls as Reversible-Action Admission

Full title: Tool Calls as Reversible-Action Admission: A Runtime Layer for Agentic AI Safety. The agentic-safety literature treats safety as a property of the model; this paper argues for an independent property: safety at the runtime that admits a tool call, independent of the model that produced it. Admission-layer safety composes with training-layer interventions such as Constitutional AI, RLHF, and scalable oversight; it does not replace them. The refusal holds even when alignment training has failed, because the runtime verifier makes the admission decision.

Each tool call falls into one of three action classes. Observational calls read state without mutating it. Reversible calls mutate state with a known inverse executor (a quarantine has a release, a row insert has a delete). Destructive calls mutate state with no typed inverse (a ledger broadcast, an external send). The runtime classifies the call, and an unclassified method is destructive by default. The runtime accepts a call wrapped in an admission envelope carrying four fields beyond its arguments: an authorization chain, an action class, a positive TTL by construction, and, for reversible and destructive classes, a typed rollback receipt slot. The envelope is typed: a reversible call without a TTL is not constructable, and a destructive call without both a TTL and a bilateral cosignature is not constructable.

Admission proceeds by four decidable operations, each with a named rejection code: a capability check (cap-denied), a class check (class-mismatch), a TTL check (ttl-invalid), and a rollback-slot check (rollback-missing) that additionally requires a bilateral cosignature for the destructive class. The paper describes three structural properties proved in the sovereignty model: a reversible or destructive envelope is well-typed only if it carries a positive TTL witness and a rollback slot; a rollback receipt that closes a previously-admitted call remains admissible under a backward-refining amendment; and a destructive call admits only if both the operator polity and the host polity admit it under their respective predicates. The last is treaty_admission_iff_predicate_intersection, the same theorem the sovereignty paper proves.

Bilateral Receipt Admission

Full title: Bilateral Receipt Admission: Cross-Organization Action Provenance with Treaty-Bound DSSE. SLSA, in-toto, Sigstore, and Rekor attest how a build output was created; this paper specifies bilateral admission under a treaty-bound predicate over identical canonical bytes. It defines a bilateral DSSE envelope carrying the predicate type chio.bilateral-cosign-invocation.v1 (the constant PREDICATE_TYPE_BILATERAL). The payload is an in-toto v1 statement; the predicate body is a ten-field binding tuple over RFC 8785 canonical JSON; the DSSE subject is a single digest SHA-256(JCS(bindingTuple)); and the envelope carries exactly two Ed25519 signature slices, one per kernel keyid, over identical bytes.

The binding tuple

Each of the ten fields commits to a distinct admission precondition: treaty-scope hash, ladder-intersection hash, admission-report hash, continuation hash, request hash, outcome hash, local-receipt hash, remote-receipt hash, the lease (epoch and expiry), and the two signer kernel ids. The treaty-scope hash pins the relationship in force so a re-presented envelope has a different hash and cannot be rerouted; the continuation hash links the envelope to prior receipt-graph state; the two receipt hashes are what distinguish bilateral admission from a unilateral attestation.

{ "_type": "in-toto-statement/v1",
  "predicateType": "chio.bilateral-cosign-invocation.v1",
  "subject": [ { "digest": { "sha256": "9f1c...e0a4" } } ],
  "predicate": {
    "treatyId":         "treaty:opus-alpha:2026",
    "treatyScopeHash":  "7b2a...c1e0",
    "ladderInterHash":  "8c4d...3f02",
    "admissionRptHash": "a91e...204b",
    "continuationHash": "5d22...8e07",
    "requestHash":      "11ff...6a91",
    "outcomeHash":      "33ee...b15d",
    "localReceiptHash": "6677...d4cc",
    "remoteReceiptHash":"8899...02ab",
    "lease": { "epoch": 412, "expiry": 1788000000 },
    "signerKids": [ "kid:opus#1", "kid:alpha#1" ] },
  "signatures": [
    { "keyid": "kid:opus#1",  "sig": "..." },
    { "keyid": "kid:alpha#1", "sig": "..." } ] }

Six gates, five rejection codes

The verifier verify_chio_bilateral_dsse_envelope in crates/trust/chio-federation/src/bilateral_dsse.rs is a total function from a candidate envelope and verifier-owned state to either a rejection code or an admission verdict. It accepts if six gates hold in order. Byte-level checks run before the verifier consults state the sender cannot see, so a sender cannot satisfy a strict subset of gates by tailoring bytes alone. The envelope layer enforces the DSSE bytes; the operational layer in crates/trust/chio-federation/src/bilateral_verifier.rs adds peer pinning, ladder-manifest freshness, revocation epoch, receipt resolution, and lease checks. A signature-bytes failure denies before the six gates run and is not one of the five codes.

Each code names a conjunct of the admission predicate rather than a per-field diagnostic: subject-digest-mismatch rejects sibling-treaty cross-receipt substitution, signer-reuse rejects the confused-deputy cosignature, predicate-type-mismatch rejects profile downgrade, and stale-lease rejects post-revocation replay by reading the verifier's own epoch rather than any field in the envelope.

Lean accept-set transcription

A machine-checkable transcription of the accept relation lives at formal/lean4/Chio/Chio/Treaty/BilateralAccept.lean. It strips the runtime to a trust store, a bilateral envelope, and a denotational interpreter for the scope predicate, then collapses the six runtime gates into three abstract conjuncts: issuer-key membership, kernel-key membership, and the scope denotation. The main theorem is freestanding_accept_set_theorem, with three definitional corollaries (accept_monotone_in_issuer_store, accept_conj_scope_decompose, accept_requires_issuer_key). Its axiom footprint under #print axioms is propext, Classical.choice, and Quot.sound, which are assumptions used by Mathlib developments.

Reproducing the Materials

The repository contains build inputs for each paper. Build a paper PDF from its directory:

$ cd docs/papers/programmable-sovereignty
$ pdflatex paper.tex && bibtex paper && pdflatex paper.tex && pdflatex paper.tex

Build and axiom-check the sovereignty Lean supplement with elan installed. A cold cache takes roughly three to five minutes and finishes without warnings, without sorry, and without any project-local axiom:

$ cd docs/papers/programmable-sovereignty/supplementary
$ tar xzf lean-source.tar.gz
$ cd chio-lean && lake build

Exercise the runtime and the closure directly against the workspace. The admission hook's replay edge is covered by crates/kernel/chio-runtime-core/tests/runtime_admission.rs, and the replay corpus asserts manifest stability across machines:

# 50-fixture replay corpus, manifest-stable across machines
$ CHIO_BLESS=0 cargo test -p chio-replay-gate --test golden_byte_equivalence

# per-path microbenchmarks (writes bench/results/)
$ ./docs/papers/programmable-sovereignty/bench/run-treaty-intersection.sh

The Lean toolchain is pinned at leanprover/lean4:v4.28.0-rc1, the same pin the production Lean proofs use, so the paper supplement and the shipped proof root compile under one toolchain.

Where the Papers Sit in the Formal Section

The papers narrate the same objects the rest of this section catalogs. The theorems they name appear, with per-theorem status, in the Theorem Inventory. The Lean conventions and project layout are covered in Lean 4 Proofs, and the trust boundary the bilateral transcription defers to is the Assumptions and TCB page. For the layered picture of what is proven versus tested, start at the Formal Assurance Overview.

• Bilateral Federation · the treaty and cross-organization admission relation formalized by the bilateral paper.
• Capabilities · the attenuating authority tokens the polity roster C is built from.
• Receipts · the canonical, signed records the admission scope T is closed over.
• Trust Model · where formal assurance sits inside the zero-ambient-authority design.