Coalgebraic self-custody
A machine-checked law of motion for autonomous capital.
Abstract
Autonomous agents are beginning to manage capital at scale, yet the dominant safety story remains empirical: systems are tested, not proven, and the operative failure modes — key compromise, policy drift, and model hallucination — are precisely those that testing under-samples. We present coalgebraic self-custody, a semantics in which an autonomous capital agent is a coalgebra c : S → F_ZERO S of the polynomial endofunctor F_ZERO X = Σ A (λ a → B a → X) over a state space of governed question kinds A and admissible branches B. The agent's behavior is the unique anamorphism into the final coalgebra, and we machine-check two safety theorems in Cubical Agda under guarded recursion: (I) determinacy — any homomorphism into the final coalgebra equals the canonical unfold (lemma
unique); and (II) observational adequacy — bisimilar states have equal behavior (lemmabisimilar-states-imply-equal-Q). Both check under--safe --cubical --guardedness --no-import-sorts, with no axioms, no sized types, and no termination pragmas. Self-custody is structural: no constructor of the state space produces signing-key material, so "the agent holds its own keys" is not expressible in the model. We close the gap between proof and deployment with a content-addressed, offline, byte-reproducible type-check and a fail-closed runtime-attestation gate that rejects any live transition not equal to the proven unfold, terminating in a signed, self-issued, bounded proof card.
Claims and evidence
Every claim the paper makes maps to an exact command — or lemma — and its expected exit code, so a reviewer reproduces each claim mechanically rather than taking it on trust. Claims carry one of three tags:
- PROVEN — mechanically type-checked or replay-verified by exit code at the cited commit
- TRUE — holds by construction
- NEAR — roadmap, stated as such; never presented as done
The two theorems check in Cubical Agda under a safe flag set with no axioms, no sized types, and no termination pragmas. The type-check is offline and byte-reproducible against a content-addressed, vendored dependency closure: tampered or missing dependency bytes are rejected before checking begins. The runtime side is fail-closed — a live transition is rejected unless it equals the proven unfold, and negative fixtures confirm the gate rejects illegal edges, custody-violating edges, and tampered signatures.
Honest scope
The proof card the system issues is self-issued and bounded — scoped subject, deterministic id, expiry, revocation pointer. It is not independent or third-party certification, and the paper does not present it as such. Attestation over live production traffic, real external issuance, and on-chain revocation are roadmap items, gated fail-closed until real evidence exists.
Artifact
The artifact ships with a step-by-step reproduction runbook and a one-command, network-free Docker setup. The claims-to-evidence table is itself replayable: each row records the command and observed exit code at the commit reproduced, so the table never asserts more than the checker verifies.
The arXiv link will appear here once the submission is public. Until then: hi@degenie.xyz.