Environment Assumptions

A machine-checked proof covers the model it was run on. Where that model meets the world (keys, clocks, the database, the machine the code runs on), the proof holds only while the world behaves as assumed. This page names each of those assumptions, how ICA meets it in production, and how you can check it yourself. Every figure below was measured on 28 September 2026.

The first three

Signing-key custody, the time-stamp authority’s clock, and the window before a receipt is anchored come first, because they are where trust in the ledger rests.

1. Custody of the signing keys

• Assumed: only ICA’s signing service can sign with a current ICA key.
• In place: the Ed25519 key that signs receipts is held in HashiCorp Vault Transit. ICA asks Vault to sign, and the private key never enters the ICA service. All 241,539 receipts written in the seven days to 28 September were signed this way. Anchored ledger roots carry a second signature from a key held in AWS KMS, a separate custody domain.
• What bounds it: a key holder could sign a new receipt. Changing a receipt that is already inside an anchored root would contradict a record held outside ICA (items 2 and 3). Retired keys stay published, with the date each was retired.
• Check it: the trust anchor lists every key, current and retired, with its fingerprint. Save a copy and confirm its fingerprints. The first copy comes from ALEETH. From then on, the published verifier checks a receipt’s Ed25519 signature against your saved copy, offline.

2. The time-stamp authority’s clock

• Assumed: the outside clocks that date the ledger tell the truth.
• In place: two independent sources date the ledger. An RFC 3161 time-stamp authority, FreeTSA, stamps the latest anchored root at every service start and every 24 hours: 111 tokens in the seven days to 28 September. Each root is also carried into a chain of seals that OpenTimestamps commits to Bitcoin. All 24,677 seals are confirmed, with a median of about one hour from seal to block.
• What bounds it: the two sources share nothing. A time-stamp clock that drifts far from Bitcoin shows up when you compare the two for the same root, and Bitcoin sets an outside bound of its own: a root existed no later than the block that carries it.
• Check it: transparency status shows the latest token, its time, and the signature and chain results. Any OpenTimestamps client checks a seal against Bitcoin.

3. The window before a receipt is anchored

• Assumed: until a receipt’s root is anchored and sealed, nobody with owner rights on the database rewrites or removes it.
• In place: inside that window a receipt rests on its own signature, a hash chain that links it to the receipt before it in its session, and database rules that refuse every update and delete. Roots are anchored every six hours and at every service start, and a Bitcoin seal follows each anchor. In the 30 days to 28 September, every anchor window but one closed within six hours and a minute. The exception, on 6 September, ran 8.2 hours. In the seven days to 28 September, the Bitcoin block followed within 2.6 hours of the seal.
• What bounds it: once a root is anchored, changing any receipt under it changes the root. On 28 September we recounted every window anchored in the previous 30 days against the leaf count recorded when it was anchored. All 587 matched exactly.
• Check it: open this receipt’s inclusion proof and recompute its anchored root offline. Put any receipt hash in that address to check another. A leaf is the SHA-256 of the byte 0x00 followed by the receipt hash as lowercase hex text. An inner node is the SHA-256 of the byte 0x01 followed by the left and right child digests. The same receipt’s chain of custody follows it out to Bitcoin.

What the gateway proofs take as given

4. The request is resolved from true facts

• Assumed: the facts a decision is made on are true: the agent’s state, its tenant, its signed contract, its allow and deny lists, the class of the action, whether the action rests only on untrusted content, the health of its dependencies, and any human approval. The proof covers what the gateway decides with those facts.
• In place: agent state is read fresh for every Tool Gateway decision. In the Tool Gateway, unclassified and irreversible actions are denied by default, and an unhealthy dependency means a consequential action is denied.
• What bounds it: adversarial harnesses for tenant isolation, cross-tenant access and fail-closed behaviour run inside the proof gate that every change to ICA must pass before it merges.
• Check it: ICA publishes authenticated-route coverage for ALEETH’s own platform routes, including the routes it does not govern. It does not measure policy enforcement.

5. The running code is the checked code

• Assumed: production runs the same decision code that was checked.
• In place: after the model is checked, the real decision function runs on every change over 2,592 requests, every combination of agent state, tenant, contract shape, action class, dependency health, the agent’s assessment and budget. Every answer is held to the conformance checks, which the property catalog lists one by one with the property each covers. A fingerprint of its full decision table is compared with the approved baseline. A change that grants authority the baseline withheld is refused unless a person approves that exact fingerprint. A release identity attestation binds the deployed build to its source, and the running service recomputes its own fingerprint.
• What bounds it: the build pipeline and the hosting platform are assumed to run what was built. The running service’s own fingerprint notices any change in what the decision function decides.

6. What exhaustive means here

• Assumed: the decision model’s input space is finite, and the checker covers all 1,152 requests in it. The single-use capability is checked over a bounded set of capabilities under every interleaving, and mission authority over three capabilities and two people, 21,248 states. Larger configurations are assumed to behave like the checked ones.
• In place: 15 red twins, each a copy of a model with one guard removed, run in the same suite. Each must produce a counterexample, or the suite fails.
• Safety first: the properties say nothing unauthorised happens. When a dependency fails, the designed outcome is a refusal.

Single-use capabilities

7. The burn is atomic

• Assumed: checking that a capability is unused and marking it used happen as one step.
• In place: production does both in one conditional database update that succeeds only while the capability is unused and unexpired. Of two concurrent attempts, one succeeds and the other changes nothing. This relies on a single primary Postgres database, which is how ICA runs. Expiry is judged by ICA’s own clock.
• What bounds it: a capability runs at most once, for the exact arguments it was issued for. If the service stops after the burn, the action does not run, and it is never repeated.

The ledger

8. Cryptography and canonical bytes

• Assumed: SHA-256, Ed25519, ECDSA P-256 and ML-DSA-65 hold, and every verifier turns a receipt into the same canonical bytes (sorted keys, no whitespace).
• In place: the Merkle tree separates leaves from inner nodes with distinct prefixes and promotes an odd node instead of duplicating it, which closes the duplicate-leaf attack of CVE-2012-2459. Each anchor records the order its leaves were taken in.

9. Append-only storage

• Assumed: nobody with owner rights on the database switches off the rules that refuse updates and deletes on receipts, the audit chain and the seals.
• What bounds it: before a root is anchored, this is the window in item 3. After it is anchored and sealed, any change contradicts a record held outside ICA.

10. Everyone sees the same log

• Assumed: ICA shows every verifier the same anchored roots.
• In place: each root names the root before it. Across all 985 anchors, no two name the same predecessor, and since 1 September 2026 the chain is continuous. Since 7 September 2026, each root is carried to Bitcoin through OpenTimestamps, by its own seal or by a later root that names it.
• Check it: the anchor list publishes every root and the root it names. Keep the roots you verify, and any two verifiers can compare what they hold.

11. The right public keys

• Assumed: you hold ICA’s real public keys.
• In place: the trust anchor lists them with fingerprints. Save a copy and confirm its fingerprints. ALEETH does not publish the fingerprints through a second channel, so the first copy comes from ALEETH. From then on, the published verifier checks a bare receipt against your saved copy without fetching keys from ICA.

Where to check

• aleeth.com/verify: verify a credential and watch ICA recompute its audit chain.
• Transparency status: the latest anchored root and its RFC 3161 token.
• Anchor list: every anchored root and the root it names.
• Trust anchor: every public key, current and retired.
• Authenticated-route coverage: the side-effecting ALEETH platform routes that pass an identity control, and the declared gaps. It does not measure in-path approval decisions.
• Formal artifacts: the TLA+ specifications, their red twins and the conformance harnesses, to read and re-run.