Research Papers

The paper sources

Each directory under docs/papers/ holds a paper.tex, its sections/, and a built paper.pdf. The title column is the \title of that paper.tex, which is not always the directory name.

Receiver-owned bilateral admission

Directory: docs/papers/programmable-sovereignty/. A vendor agent returns a correctly signed receipt, and the buyer still has to reject it if it belongs to another treaty, binds different arguments, follows an expired continuation, omits required lineage, or records a policy result the buyer does not accept. The paper's argument is that a signature identifies a key rather than deciding whether the receiver should admit the action, and that an audit after execution is too late once the tool has already changed the vendor ledger. Receiver-owned admission moves the decision into the receiving kernel before dispatch.

Three objects combine in a stricter order than usual. A receipt is a kernel-signed record of a mediated tool decision over canonical bytes. A treaty fixes the participants, keys, permitted action classes and validity period. A bilateral predicate is a canonical DSSE statement signed by two configured keys and bound to the request, outcome, treaty, continuation, lineage and both receipt digests. The receiver checks that predicate only after loading the referenced state from its own stores. The paper states its own limit in the same paragraph: two distinct keys over the same bytes are necessary but do not prove independent organizational control, and key custody remains a deployment assumption.

The Lean development

The Lean model is small and deliberately so. It specifies a predicate library over a receipt view already built from validated artifacts, with nine atom forms testing receipt identity, participant membership, action class, minimum ladder rank, receipt hash, live continuation membership, decision, failure code, and an evidence-class and digest pair. A constitution is a finite list of predicates and admission is their conjunction. Signature verification, canonical serialization, clocks, durable storage and the construction of the receipt view all sit outside the model, in the implementation.

The supplementary package pins exactly which declarations the paper stands on. It is two theorems, both in formal/lean4/Chio/Chio/Treaty/ReceiptPredicate.lean, both classed bounded_theorem, with their Lean axiom footprint recorded per theorem:

[manifest]
schema = "chio.programmable-sovereignty.proof-manifest.v1"
generated_at = "2026-07-26"
paper = "Receiver-Owned Bilateral Admission for Cross-Organization Agent Tool Calls"
target_venue = "USENIX Security 2027 Cycle 1"
lean_toolchain = "leanprover/lean4:v4.28.0"
model_boundary = "bounded receipt predicates and supplied finite domains"
implementation_relation = "independent Rust differential testing, not extraction or refinement"

[[theorems]]
id = "PS-F01"
name = "finite_refinement_sound"
lean_module = "Chio.Treaty.ReceiptPredicate"
lean_declaration = "Chio.Treaty.ReceiptPredicate.finite_refinement_sound"
path = "formal/lean4/Chio/Chio/Treaty/ReceiptPredicate.lean"
claim_class = "bounded_theorem"
axioms = ["propext", "Quot.sound"]
scope = "A successful check preserves the current admission result for every receipt in the supplied finite domain."

[[theorems]]
id = "PS-F02"
name = "finite_refinement_exact"
lean_module = "Chio.Treaty.ReceiptPredicate"
lean_declaration = "Chio.Treaty.ReceiptPredicate.finite_refinement_exact"
path = "formal/lean4/Chio/Chio/Treaty/ReceiptPredicate.lean"
claim_class = "bounded_theorem"
axioms = ["propext", "Quot.sound"]
scope = "The Boolean checker is equivalent to the finite-domain admission implication."

lean_toolchain there is the same leanprover/lean4:v4.28.0 that formal/lean4/Chio/lean-toolchain pins for the shipped proof root, so the supplement and the root compile under one toolchain. implementation_relation is the field to read before quoting the theorems anywhere else: it says independent Rust differential testing, not extraction or refinement.

Runtime and closure

The receiver's control flow runs the kernel's capability, scope, revocation, budget and guard checks first. A cross-organization request then enters ChioRuntimeAdmissionHook::evaluate, which implements the RuntimeAdmissionHook trait declared at crates/kernel/chio-kernel/src/kernel/mod.rs. It loads the referenced artifacts, checks the treaty and continuation, verifies the bilateral statement, and returns either a named denial or an accepted result. The tool server is invoked only after all of that succeeds.

Three behaviors carry the paper's argument. treaty_ref_from_request, in crates/kernel/chio-runtime-core/src/admission_hook/treaty_ref.rs, rejects request-carried trust roots, peer directories, signing keys, revocation records and dynamic trust bundles, accepting only identifiers it then resolves through the receiver's own stores. Malformed or missing federated context denies rather than falling back to the local path. And the hook reserves a continuation while admission is in progress, consumes it before an admitted dispatch, and releases it after a pre-dispatch denial or abort, so a continuation that was admitted and then aborted cannot be replayed under a fresh request.

Treaty validation itself lives in crates/kernel/chio-runtime-core/src/treaty.rs, where validate_treaty_scope rejects unsupported schemas, invalid validity windows, and missing or duplicate participants, and compute_ladder_intersection builds the joint action-class table. The three-vendor example is generated by examples/chio-3vendor/src/main.rs and exercised end to end by scripts/check-chio-live-treaty-buyer-closure.sh.

Evaluation

Two scripts under docs/papers/programmable-sovereignty/bench/ produce every reported number. run-bilateral-admission.sh performs two warmups, then the complete-workflow and per-component samples, retaining raw CSV, machine and toolchain metadata, a JSON summary and generated TeX macros under bench/results/. run-replay-corpus.sh reports the generic capability corpus and the bilateral negative matrix separately. The paper's Method section names the baseline machine as Linux on aarch64 with eight Arm Neoverse-N1 cores and 49.2 GB of RAM, and pins the rustc and cargo versions it measured under, with bilateral measurements taken in the release profile.

The four research questions are: whether the implementation rejects the threat-model attacks before dispatch, whether the independent Rust reference interpreter agrees with the runtime bounded evaluator, what the pre-dispatch denial path and the complete local buyer workflow cost, and what replay coverage and package size are. The retained result files report a pre-dispatch treaty denial at 11.124 ms p50 and 20.530 ms p99, a complete local buyer workflow at 2.488 s p50 and 3.291 s p99, 20 complete-workflow samples and 30 component samples, and a 51,843-byte buyer package.

The 2.488 s figure is the one to read carefully. The evidence ledger says so itself: it includes three-vendor process orchestration, SQLite, package generation, buyer CLI startup, schema validation and semantic review, and it is not receiver-hook latency.

- Two configured keys do not prove two independent organizations.
- The Lean development does not verify the Rust runtime.
- A finite test domain does not cover receipts omitted from that domain.
- The single-host experiment does not estimate wide-area or concurrent
  deployment behavior.
- The buyer package does not prove remote process integrity or legal effect.

Tool calls as reversible-action admission

Directory: docs/papers/agentic-tool-safety/. The agentic-safety literature treats safety as a property of the model; this paper argues for an independent property: safety at the substrate 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 rather than replacing them. The refusal holds even when alignment training has failed, because the substrate 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 transaction broadcast to a public ledger, an email to an external recipient). The classification is the substrate's commitment rather than the agent's, and an unclassified method is destructive by default. The substrate 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, so 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. Rejection at any gate emits a receipt carrying the named code.

The paper's worked-example section is a sketch and says so. It walks two calls in prose to argue that the grammar is implementable on existing components, and states that it does not benchmark, evaluate or measure, and does not defend a particular implementation as load-bearing. The reversible example deletes a git branch under a 24-hour TTL with a re-creation-from-SHA rollback executor. The destructive example issues a db.dump to an untrusted bucket and is refused at the rollback-slot gate because the inverse witness is not constructable against the destination's trust store, so the bilateral cosignature gate is never reached. What the substrate verifies there is constructibility of the inverse witness, not intent.

Bilateral receipt admission

Directory: docs/papers/bilateral-receipt-admission/. 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. The envelope is a DSSE statement carrying the predicate type chio.bilateral-cosign-invocation.v1, which the implementation holds in the constant PREDICATE_TYPE_CHIO_BILATERAL_INVOCATION in crates/trust/chio-federation/src/bilateral_dsse/types.rs. The payload is an in-toto v1 statement, the DSSE subject is a single digest whose preimage is the canonical hash of the predicate body, and the envelope carries exactly two Ed25519 signature slices, one per kernel keyid.

The binding tuple

Each field of the tuple commits to a distinct admission precondition. The treaty-scope hash pins the participant identities, named action classes and lifetime in force, so re-presenting the envelope under a different relationship is a hash miss rather than a re-routable token. The ladder-intersection hash pins which action class was evaluated at which mode, so a sender cannot retroactively claim a lower floor than both sides agreed to. The admission-report hash pins the receiving polity's intent: which predicates it checks, which evidence it requires, which fail-closed codes it has pre-declared. The continuation hash names the prior receipt this envelope extends. The request and outcome hashes commit to input and output bytes separately, so selective disclosure can reveal one without the other. The local-receipt and remote-receipt hashes are what distinguish bilateral admission from a unilateral attestation. The lease commits to a revocation epoch and an expiry, and the signer kernel ids prevent post-facto reassignment to a different pair.

The paper prints a worked envelope with placeholder hashes, which is the shape a verifier parses:

{ "_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": "..." } ] }

Two verifier layers, five rejection codes

verify_chio_bilateral_dsse_envelope, in crates/trust/chio-federation/src/bilateral_dsse/verify.rs, is a total function from a candidate envelope and verifier-owned state to either a rejection code or an admission verdict binding the two named cosigners to canonical bytes. Its gates split into two layers, and the ordering between them is load-bearing: every byte-level check fires 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 payload-type equality against the bilateral statement type, a signature count of exactly two, canonical-JSON equivalence between the inner payload and its declared digest, predicate-type equality, single-subject presence, and keyid distinctness across the two signatures. The operational layer in crates/trust/chio-federation/src/bilateral_verifier.rs accepts only envelopes that already cleared the envelope layer, then gates them against peer key pinning, ladder-manifest freshness, revocation epoch, receipt resolution, request and tool-argument hashes, policy verdict agreement, capability lease, receipt-backed-class governance receipts, and treaty binding identifiers.

Five rejection codes name where a candidate failed. The paper maps each to its layer:

Each code names a conjunct of the admission predicate rather than a per-field diagnostic, because an audit consumer has to tell a wrong predicate type from a degenerate signer reuse from a stale lease from a sibling-treaty digest disagreement; each names a different precondition with a different remediation. The paper also names what sits outside the construction's threat model: it binds two honest cosigners to canonical bytes against an arbitrary network adversary, and a single actor controlling both signing keys, whether through key-custody compromise or one vendor operating both ends, is independent of every gate in the verifier.

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 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). Running #print axioms against the theorem and each corollary reports only propext, Classical.choice and Quot.sound, the trusted base every Mathlib development presupposes.

Reproduce

Two of the three directories build with the same LaTeX sequence their README.md names:

cd docs/papers/bilateral-receipt-admission
pdflatex paper.tex && bibtex paper && pdflatex paper.tex && pdflatex paper.tex

The receiver-owned admission directory is different. It carries a Makefile, and paper-usenix.tex is its submission source while paper.tex is an ACM-style fallback. Its build target runs the complete LaTeX and BibTeX build, checks references and citations, and enforces a 13-body-page limit:

cd docs/papers/programmable-sovereignty
make submit-check

The artifact check is the more useful command, and it runs from the repository root. In check mode it regenerates the artifact, verifies every file, symbol, theorem, script, result and hash, extracts the Lean archive into a private temporary directory and runs lake build there. --full additionally rebuilds the proof root, the differential tests, the runtime and federation tests, the live buyer closure, the bilateral and replay experiments, and the PDF, writing fresh measurements to a temporary directory so reproduction does not overwrite the recorded results:

bash scripts/check-programmable-sovereignty-artifact.sh
bash scripts/check-programmable-sovereignty-artifact.sh --full

Expect different latency samples from a new run. The supplementary README says as much: the benchmark is machine-local, and a fresh run should preserve schemas, case counts, non-dispatch assertions and proof-package structure rather than reproduce the numbers.

See also

The papers narrate 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 in Lean 4 Proofs, and the trust boundary the bilateral transcription defers to on the Assumptions and TCB page. For the layered picture of what is proved against what is tested, start at the Formal Assurance Overview.

• Bilateral Federation · the treaty and cross-organization admission relation the bilateral paper formalizes.
• Capabilities · the attenuating authority tokens an authorization chain is built from.
• Receipts · the canonical, signed records a bilateral predicate binds.
• Trust Model · where formal assurance sits inside the zero-ambient-authority design.