Research Papers

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 when it belongs to another treaty, binds different arguments, follows an expired continuation, omits required lineage, or records a policy result the buyer refuses. The paper argues that a signature identifies a key and leaves the admission decision open, and that an audit after execution comes too late once the tool has changed the vendor ledger. Receiver-owned admission moves the decision into the receiving kernel, before dispatch.

Three objects combine in a strict order. 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 it only after loading the referenced state from its own stores. The paper states its limit in the same paragraph: two distinct keys over the same bytes are necessary, independent organizational control needs more, and key custody remains a deployment assumption.

Lean development

The Lean model is deliberately small. It specifies a predicate library over a receipt view already built from validated artifacts, with nine atom forms: 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 construction of the receipt view sit in the implementation, outside the model.

The supplementary package pins the declarations the paper stands on: two theorems in formal/lean4/Chio/Chio/Treaty/ReceiptPredicate.lean, both classed bounded_theorem, each with its recorded Lean axiom footprint.

[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."

Its lean_toolchain 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. Read implementation_relation before quoting the theorems elsewhere: it says independent Rust differential testing, not extraction or refinement.

Runtime and closure

The receiver 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 in crates/kernel/chio-kernel/src/kernel/mod.rs. The hook loads the referenced artifacts, checks the treaty and continuation, verifies the bilateral statement through verify_chio_bilateral_dsse_envelope, and returns a named denial or an accepted result. The tool server is invoked only after all of that succeeds.

Three behaviors carry the 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, and accepts only identifiers it then resolves through the receiver's own stores. Malformed or missing federated context is denied, with no fallback to the local path. 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 an admitted-then-aborted continuation cannot be replayed under a fresh request.

Treaty validation lives in crates/kernel/chio-runtime-core/src/treaty.rs: validate_treaty_scope rejects unsupported schemas, invalid validity windows, and missing or duplicate participants, and compute_ladder_intersection builds the joint action-class table. examples/chio-3vendor/src/main.rs generates the three-vendor example, and the live treaty buyer-closure check exercises it from request to buyer package before every release. Two-Org Worked Example runs the same admission with the installed CLI.

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, and retains 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 Method section names the baseline machine as Linux on aarch64 with eight Arm Neoverse-N1 cores and 49.2 GB of RAM, pins the rustc and cargo versions, and takes bilateral measurements in the release profile.

The four research questions ask 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 evidence ledger scopes the 2.488 s figure: it includes three-vendor process orchestration, SQLite, package generation, buyer CLI startup, schema validation, and semantic review, and is distinct from receiver-hook latency.

Recorded limits

docs/papers/programmable-sovereignty/CLAIM_LEDGER.md closes with what the paper leaves unestablished, verbatim:

- 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 a property of the layer 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, and the refusal holds when alignment training has failed, because the admitting layer makes the 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, such as a transaction broadcast to a public ledger or an email to an external recipient. The classification is the admitting layer's commitment, never the agent's, and an unclassified method is destructive by default.

A call arrives in an admission envelope carrying four fields beyond its arguments: an authorization chain, an action class, a positive TTL by construction, and, for the reversible and destructive classes, a typed rollback receipt slot. The envelope is typed, so a reversible call without a TTL and a destructive call without both a TTL and a bilateral cosignature are each unconstructable.

1. Capability check. Rejects with cap-denied.
2. Class check. Rejects with class-mismatch.
3. TTL check. Rejects with ttl-invalid.
4. Rollback-slot check. Rejects with rollback-missing, and for the destructive class also requires a bilateral cosignature.

Admission proceeds by these four decidable operations. Rejection at any gate emits a receipt carrying the named code.

Structural commitments

The paper names three structural commitments and discharges their proofs in cited companion work. It scopes the first itself: the claim that a reversible or destructive envelope is well-typed only with a positive TTL witness and a rollback slot is “a definitional bridge documenting the type-level invariant”, whose substantive use is the type checker refusing to construct envelopes without the discipline.

The third commitment, treaty admission iff predicate intersection, resolves to treaty_admission_iff_predicate_intersection, a proved Lean theorem in formal/lean4/Chio/Chio/Treaty/Intersection.lean. The theorem inventory records it as proof.treaty_admission_iff_predicate_intersection with claim class bounded_model, status proved, mapping to P3. Bounded model is the operative phrase: the theorem is about the Lean model, and the Rust that implements it carries separate evidence.

Worked example

The 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 it neither benchmarks, evaluates, nor measures. 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 cannot be constructed against the destination's trust store; the bilateral cosignature gate is never reached. The admitting layer checks that the inverse witness can be constructed, which says nothing about 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, held 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 same module emits a second, compatibility profile, chio.bilateral-signature-slice.v1, held in the constant PREDICATE_TYPE_BILATERAL. The two are deliberately distinct, as the module docstring states. A keyid in either profile is the SHA-256 fingerprint of a kernel passport public key rendered as lowercase hex.

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. The ladder-intersection hash pins which action class was evaluated at which mode, so a sender cannot later 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, and 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 distinguish bilateral admission from a unilateral attestation. The lease commits to a revocation epoch and an expiry, and the signer kernel ids prevent later reassignment to a different pair. The paper prints a worked envelope with elided hash values, in 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": "..." } ] }

Verifier layers and 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 a rejection code or an admission verdict that binds the two named cosigners to canonical bytes. Its gates split into two ordered layers: 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 checks 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, a single subject, and keyid distinctness across the two signatures. The operational layer in crates/trust/chio-federation/src/bilateral_verifier.rs accepts only envelopes that cleared the envelope layer, then checks 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. An audit consumer has to tell a wrong predicate type from a degenerate signer reuse, a stale lease, or a sibling-treaty digest disagreement, because each names a different precondition with a different remediation. The construction binds two honest cosigners to canonical bytes against an arbitrary network adversary; a single actor controlling both signing keys, through key-custody compromise or one vendor operating both ends, sits outside its threat model, and no gate in the verifier tells it apart from two honest cosigners.

Lean accept-set transcription

A machine-checkable transcription of the accept relation lives in formal/lean4/Chio/Chio/Treaty/BilateralAccept.lean. It reduces 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, and 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.

The paper calls that axiom footprint a hygiene claim: every Lean development free of sorry and custom axiom declarations shares it, and its audit value is that a later strengthening of the module shows up as an axiom-footprint diff against this baseline. The module records the acceptance relation. Ed25519 byte-level soundness, SHA-256 collision resistance, JCS injectivity, Rust-to-Lean refinement of verify_chio_bilateral_dsse_envelope, and the polity-level treaty and amendment properties sit in the audited trust base.

The higher-layer statements live elsewhere. The paper's related work cites treaty_admission_iff_predicate_intersection from a separate manuscript that places the bilateral primitive inside a polity model; the theorem itself is proved in formal/lean4/Chio/Chio/Treaty/Intersection.lean.

Reproduction

Read the receiver-owned admission paper as a PDF. Each directory under docs/papers carries its built paper.pdf beside the LaTeX source, and its README.md names the build sequence.

The programmable-sovereignty artifact check runs before every release is tagged. It regenerates the artifact, verifies every file, symbol, theorem, script, result, and hash, extracts the Lean archive into a private directory, and runs lake build there; its full mode also rebuilds the proof root, the differential, runtime, and federation tests, the live buyer closure, the bilateral and replay experiments, and the PDF. The proof report records the result, and chio release verify --evidence formal checks it for the release you run. Maintainers run the check from source as Qualification: formal gates describes.

The supplementary README describes the benchmark as machine-local: a fresh run preserves schemas, case counts, non-dispatch assertions, and proof-package structure, and its latency numbers vary with the machine.