Security evidence you can rerun

Gate makes one narrow preventive claim: on a completely mediated protected path, a mutation that lacks the owner's required exact-action evidence does not reach the provider. The public security case tests that claim with 35 executable claims, bounded formal models, negative vectors, fault schedules, and byte-pinned release evidence. Every count below is generated from the current repository.

Shipped

Each item below is verifiable today — reproducible by anyone from the public repo or directly inspectable on this site.

Conditional roadmap

These items are being scoped or are conditional on a funded engagement. A target is shown only when the named prerequisite exists; an unfilled auditor or sponsor field is not a commitment, certification, or buyer claim.

Future intent

Targeted certifications and frameworks sequenced against named pilot or sponsor engagement. We treat these as commitments to pursue when the corresponding buyer relationship is real, not as marketing claims.

Formal verification

The strongest result is compositional: one Tamarin Dolev-Yao model follows a signed challenge through CAID, two distinct approvals, issuer and authority pins, an exact registry view, revocation, one-time consumption, and execution. It verifies 20 obligations under its stated assumptions.

The model also keeps 8 intentionally weakened comparison obligations. Remove consumption and Tamarin finds same-receipt replay. Stop pinning the exact registry head and epoch and it finds a stale or equivocating authority-view acceptance. Those counterexamples demonstrate that the controls are load-bearing rather than decorative.

Separately, TLA+ checks 26 authorization-state invariants and Alloy checks 35 facts plus 32 assertions. These models run in CI alongside executable negative vectors. A model failure or security-case mismatch fails the build; the proof record lives beside the implementation, not in a detached paper.

What the proofs do — and don’t — cover

A guarantee you have to overstate isn’t one. So, precisely:

What they prove. Under each model's stated assumptions, accepted authorization artifacts remain bound to the modeled exact action, required signer set, freshness, authority view, and one-time consumption rules. The executable negative cases reject the named replay, substitution, downgrade, and tampering conditions.

What they do not prove — stated plainly:

• Not a proof of model behavior. The checked invariants constrain what the modeled protocol allows, not what an AI model attempts. They say nothing about whether an LLM makes good decisions — only what the modeled gate permits under its stated assumptions.
• Not a proof of deployment. If the gate runs inside a process the agent’s operator fully controls, that operator can route around it — true of any in-process check. The enforcement guarantee is end-to-end only when the system of record (the bank API, the benefits system, the deploy pipeline) verifies the authorization receipt (formerly Trust Receipt) before it executes. Until that integration exists, EMILIA is a strong default and an offline-verifiable evidence layer — not a physical barrier.

We lead with this because it’s the first question a serious reviewer asks — and because the receipt is trustworthy precisely to the extent that we’re exact about what it attests.

Responsible disclosure

Security findings on the protocol, the reference runtime, the SDKs (@emilia-protocol/sdk, @emilia-protocol/verify), the MCP server, or any *.emiliaprotocol.ai surface should be reported privately first.

• Email: security@emiliaprotocol.ai
• Disclosure metadata: /.well-known/security.txt (RFC 9116). Encrypted reports are accepted; request our PGP key in your initial email and we will respond with the fingerprint before you send sensitive details.
• Acknowledgement: within 48 hours.
• Coordination: minimum 90-day embargo on disclosure for any finding requiring a coordinated patch; we publish the advisory + credit on resolution.
• Safe harbor: we will not pursue legal action against good-faith research that follows this disclosure process and avoids privacy violations, data destruction, or service degradation.

A formal bug-bounty program (HackerOne or Immunefi) is in roadmap. Until launched, the address above is monitored and triaged.

Operational practices

• Source control: GitHub with required code review + signed commits on the reference runtime.
• CI gating: lint, type-check, unit tests, integration tests against Postgres, semgrep, CodeQL, npm audit, secret scanning, formal-verification suite, and conformance suite — all wired in CI.
• Dependencies: Dependabot enabled with auto-merge for vetted minor + patch upgrades.
• Cryptography: Ed25519 for receipt signatures, ECDSA P-256 (WebAuthn) for device signoffs, SHA-256 over deterministic (sorted-key) canonical JSON for action hashing, Merkle batching for trust-receipt anchoring. No custom crypto primitives.
• Secrets handling: no production secrets in source; secrets stored in Vercel + Supabase secret managers with least-privilege scoped roles.
• Data minimization: trust receipts contain only the bound action context and signatures; no PII unless an integrator's policy explicitly includes it (and that integrator's DPA governs that data).

Procurement & assurance documents

Requestable under NDA for active procurement engagements:

• Filled Shared Assessments SIG Lite questionnaire
• Sub-processor list (also public at /legal/sub-processors)
• DPA template (also public at /legal/privacy as the working version)
• Incident-response playbook
• Business-continuity / disaster-recovery summary
• Penetration-test summary letter (once external review is complete)
• NIST 800-53 Rev. 5 control mapping
• FFIEC IT Examination Handbook alignment notes (FinGuard) and OMB Circular A-123 alignment notes (GovGuard)

Request via security@emiliaprotocol.ai.