EMILIA is the authorization-receipt layer for irreversible AI-agent actions: no valid human-signed receipt, no execution — and afterward, anyone can verify who approved exactly what, without trusting us. This page is where you try to prove that wrong.
We claim EMILIA’s authorization ceremony cannot be replayed, forged, self-approved, or reversed — and we proved it with a model checker. Don’t take our word for it. The protocol is open. The receipts are public. Try to break it.
Safety infrastructure earns trust by surviving attack in the open. Every confirmed break — and its fix — gets published here, with credit.
The honesty is the credential. Here is exactly where the guarantee starts and stops.
Run the negative cases yourself: npx @emilia-protocol/crash-test issues a genuine receipt, verifies it offline, then shows the forged copy being rejected.
In an adversarial pass we found that a leaked receipt_id could let another authenticated actor attach their own signoff flow to someone else’s receipt and self-approve it. The cryptography was sound; the authority-binding glue was not.
We closed it by binding signoff requests to the receipt creator and approvals to the intended approver — now row four of the matrix above. We publish this on purpose: the danger zone for systems like this is authority binding and deployment semantics, not the math, and finding it in the open is the point of this page.
EMILIA’s differentiation is not proprietary cryptography. It is a composed, machine-rerunnable argument that the whole path holds together: challenge, canonical action, human ceremony, issuer and authority pins, revocation, one-time consumption, and execution.
Tamarin tests this as one symbolic protocol under a Dolev-Yao attacker with full network control, rather than assuming separately checked pieces compose safely.
execution_requires_full_compositionVERIFIED · ALL TRACESExecution requires challenge, exact action, approvals, pinned authority, revocation, and consumption to compose.
no_issuer_launderingVERIFIED · ALL TRACESA presenter cannot turn its own key into an accepted issuer by relabeling the artifact.
no_cross_action_profile_or_audience_replayVERIFIED · ALL TRACESValid evidence cannot be transplanted to another action, profile, or relying party.
initiator_cannot_self_approveVERIFIED · ALL TRACESThe actor initiating an action cannot fill the human-approval seat.
strict_registry_view_is_exactVERIFIED · ALL TRACESAuthority evidence must match the exact registry checkpoint pinned by the relying party.
injective_execution_with_consumptionVERIFIED · ALL TRACESOne consumed authorization maps to at most one checked execution.
unchecked_composition_is_injectiveRemove one-time consumption and Tamarin finds a same-receipt replay.
unchecked_registry_view_is_currentRemove exact registry-view binding and Tamarin accepts a stale or equivocating authority view.
Nothing prevents another team from implementing the open format. That is the distribution strategy. But a compatible envelope is not an equivalent system. Equivalence means reproducing the composed proof, strict verifier behavior, negative vectors, durable consumption, release evidence, and every assumption and exclusion. Each discovered failure becomes a permanent, machine-rerunnable obligation. That body of evidence compounds with every release.
Broader executable evidence: 26 TLA+ invariants · 35 Alloy facts + 32 assertions · 6,719 automated cases · 251 current conformance vectors.
Scope remains explicit: TLA+ and Alloy model bounded state and relational properties; Tamarin uses symbolic perfect cryptography and pinned-root assumptions. These are not proofs of AI behavior, WebAuthn internals, parser correctness, legal compliance, or deployment completeness.
The protocol, the SDK, and a public demo receipt are live now — attack those directly. Scoped challenge keys against an isolated instance open shortly; report anything you find to the address below in the meantime.
Report a break: team@emiliaprotocol.ai