Chio Research · Whitepaper
for Cross-Organization Agent Tool Calls
A correctly signed vendor record can still describe the wrong request, outcome, treaty, or continuation. Before any tool runs, the receiving kernel checks it against its own treaty state and rejects stale, replayed, or mismatched calls.
01Receiver-Owned Admission
deny before dispatch
The receiving kernel treats a counterparty-mediated-decision receipt as one predicate-model input to admission. It reconstructs the claim from verifier-owned state and rejects invalid records before dispatch.
receiver stores → treaty + keys + continuationThe receiver resolves treaty configuration, signer keys, and continuation state from its own stores. Request metadata cannot install signer keys.
crates/kernel/chio-runtime-core/src/admission_hook/store_artifacts.rssigA ∧ sigB over one canonical predicateTwo distinct configured keys sign the same DSSE predicate. The verifier rejects split or malformed statements.
crates/trust/chio-federation/src/bilateral_dsse/verify.rsrequest ∧ outcome ∧ treaty ∧ lineage ∧ receiptsThe predicate binds the request and outcome to the treaty scope, continuation, lineage, and both receipts.
crates/kernel/chio-runtime-core/src/admission_hook/treaty_evidence.rsadmit(view) ∨ deny before dispatchThe kernel evaluates the bounded view and denies missing, stale, replayed, mismatched, or policy-rejected admission records.
crates/kernel/chio-runtime-core/src/admission_hook.rs02Predicate Bindings
one canonical cross-boundary claim
The verifier does not accept a loose bag of valid signatures. It requires one canonical statement whose fields agree across the request, treaty, continuation, lineage, and receipts.
Request identifier, action class, capability, and receiver context.
The accepted or denied result and its stable failure code.
Scope hash, participant kernels, allowed actions, and ladder intersection.
A live, capability-bound continuation consumed once by the receiver.
The receipt-lineage statement and its authenticated digest.
The receiver-side mediated-decision receipt named by the predicate.
The counterparty receipt is one predicate input. A valid signature alone does not admit it.
Exactly one verified bilateral-invocation digest bound to the report.
admit(view) ⇔ verify(sigA, sigB, predicate) ∧ Ktreaty(view) ∧ Kleft(view) ∧ Kright(view)The bounded Lean result characterizes admission as structural predicate intersection. Rust tests exercise production validation around the view independently.
03Bounded Formal Results
4 headline theorems · Lean 4
These are machine-checked theorems over a bounded ReceiptView and explicit finite domains. Differential tests compare the production evaluator with an independent Rust reference; they do not turn the runtime into extracted or fully verified code.
treaty_admission_iff_predicate_intersection∀ τ r. treatyAdmits(τ, r) ⇔ treatyPredInter(τ, r)In the bounded receipt view, treaty admission is extensionally equal to the conjunction of the treaty and participant predicates.
formal/lean4/Chio/Chio/Treaty/IntersectionSyntactic.leantreaty_admission_stable_under_ladder_floorm ≥ modeFloor → admitsUnderMode(τ, m, r) = admits(τ, r)Once the declared finite ladder floor is satisfied, the mode check reduces to the treaty predicate.
formal/lean4/Chio/Chio/Treaty/IntersectionSyntactic.leanrefinesOnConstitution_iffrefinesOn(candidate, current, domain) = true ⇔ noWideningOn(domain)For the strict predicate syntax, the executable Boolean check is exact on the supplied finite receipt domain.
formal/lean4/Chio/Chio/Treaty/PredicateLang.leanbridge_decidable_soundnessdecideRefinement = true → ∀ r ∈ domain, candidate(r) → current(r)A positive finite-domain check implies semantic no-widening on that declared domain.
formal/lean4/Chio/Chio/Treaty/PredicateLang.lean04Measured Evaluation
eight-core Arm · SQLite loopback
The recorded results name a clean producer commit and hash their benchmark inputs. The full path includes receiver-owned stores, strict bilateral verification, policy evaluation, and buyer review.
2.288 s
p50 · 2.428 s p99 · 20 release-profile runs
13.406 ms
p50 · 22.826 ms p99 · 30 samples · zero tool invocations
20
Malformed, stale, replayed, smuggled, and policy-denied inputs
1,024 × 3
Predicates, constitutions, and finite refinement, plus exhaustive atoms
The buyer-closure performance test measured Ed25519 receipt signing at 242.4 μs p50 and verification at 370.2 μs p50. The paper reports the generic replay corpus and bilateral threat matrix separately.
05Scope and Source
claims, limits, source
The paper keeps production enforcement, bounded theorems, differential alignment, measurements, and operational assumptions as separate claim classes.
Two distinct configured keys may still be controlled by one actor. Organizational independence is an operational assumption.
Lean proves the named properties over ReceiptView and explicit finite domains. It is not Rust extraction or whole-runtime verification.
The measured three-vendor loopback ran on one eight-core Arm host with SQLite. It is not a wide-area deployment result.
The term names local authority over a receipt-admission boundary. It does not imply legal statehood or external institutional control.
Resolves verifier-owned state and makes the pre-dispatch decision.
crates/kernel/chio-runtime-core/src/admission_hook.rsChecks request, outcome, scope, continuation, lineage, and receipt digests.
crates/kernel/chio-runtime-core/src/admission_hook/treaty_evidence.rsVerifies two configured Ed25519 keys over one canonical predicate.
crates/trust/chio-federation/src/bilateral_dsse/verify.rsEvaluates the strict receipt-view predicate syntax and finite refinement.
crates/kernel/chio-runtime-core/src/treaty/predicate.rsChecks the bounded theorems and compares independent Rust semantics over generated cases.
formal/lean4/Chio/Chio/Treaty/ · formal/diff-tests/tests/treaty_predicate_diff.rsPins the manuscript, theorem inventory, benchmarks, and extracted Lean archive.
scripts/check-programmable-sovereignty-artifact.shRead the full construction, bounded proofs, evaluation, and limitations in the paper.