Procurement teams cannot evaluate a vendor without a real picture of where the security and compliance work stands today and where it is sequenced next. This page lists what is shipped, what is funded and in progress, and what is intent. We update it as commitments change. We never publish target dates we cannot hit.
Shipped
Each item below is verifiable today — independently reproducible from the public repo or directly inspectable on this site.
Funded or actively being scoped. Each item shows the target window and named partner where committed; items without a named auditor or sponsor are flagged as such — we believe a missed target is more damaging than no target.
External cryptographic-protocol review of the ceremony spec
Target: Pending pilot funding · Targeting Trail of Bits / NCC Group / Kudelski Security
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.
ISO/IEC 27001
Targeted for first enterprise pilot
StateRAMP authorization
Required for state benefit-integrity programs (GovGuard buyers)
FedRAMP Moderate ATO
Pursuing federal innovation-office sandbox engagement first; full ATO sequenced against named federal sponsor and Phase II SBIR / DARPA funding
PCI DSS / NYDFS Part 500 mapping
For FinGuard treasury-controls deployments
FFIEC IT Examination Handbook alignment
For community-bank and credit-union deployments
Formal verification
The protocol is mathematically modeled in TLA+ and Alloy. The TLA+ specification declares 26 machine-checked safety invariants — handshake binding integrity, replay resistance, signoff accountability, handshake binding, replay resistance, signoff accountability, delegation, and identity continuity. The Alloy model declares 35 facts and 22 assertions covering structural invariants the TLA+ time-domain doesn't reach.
Both run in CI on every change to the formal models. A counterexample fails the build. The model is part of the codebase, not a paper attached to it.
A guarantee you have to overstate isn’t one. So, precisely:
What they prove. Protocol-level safety: a signoff is bound to the exact action, can’t be replayed or forged, can’t self-approve, and the receipt is tamper-evident. No actor following the protocol can authorize an action that wasn’t approved by an accountable, named human.
What they do not prove — stated plainly:
Not a proof of model behavior. The theorems constrain what the protocol allows, not what an AI model attempts. They say nothing about whether an LLM makes good decisions — only that a bad one still can’t cross the gate without an accountable yes.
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.
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.
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: