GateAgent GuardProtocolStandardsMCPGovGuardSovereigntyFinGuardQuorumDemoTry itVerifyPricingDocsRequest Pilot
EMILIA Engineering Evidence

Security claims you can execute, not architecture you have to trust.

EMILIA is implemented security infrastructure. This snapshot joins an executable claim-to-code case, a composed symbolic attacker model, TLA+ and Alloy checking, cross-language negative vectors, external Rust interoperability, and durable fault tests.

Evidence snapshot: · Generated from repository manifests; CI rejects drift.

10
Composed Tamarin obligations
2 weakened variants produce concrete attack traces
16
Executable security claims
73 hashed evidence files in one resolved case
193
Current conformance vectors
17 suites across same-team JS, Python, and Go ports
359
External hostility cases
Pinned Rust source; construction scope disclosed
5,549
Automated test cases
277 files; all platform-applicable cases pass
What was demonstrated

Six evidence layers, each answering a different failure mode.

Formal proofs do not substitute for tests, and implementation agreement does not prove construction independence. EMILIA keeps those claims separate and joins them only in the public security case.

01

Hostile-network composition

Tamarin 1.10.0 · Dolev-Yao
10 obligations verified in one model from challenge through execution

The attacker may control the network and obtain unrelated honest signatures. Under uncompromised pinned roots, execution still requires the exact challenge, action, two distinct approvals, issuer and authority pins, registry view, revocation state, and one-time consumption.

02

State-machine safety

TLC 2.19 · TLA+
26 invariants checked with no reported error

The bounded authorization state machine checks replay resistance, terminal-state behavior, signoff binding, delegation limits, and write-bypass safety.

03

Relational structure

6.0.0 (CI) · Alloy
35 facts and 22 assertions

Alloy checks structural relationships that the temporal TLA+ model does not express, including identity, signoff, receipt, and federation constraints.

04

Claim-to-code traceability

EP-SECURITY-CASE-SOURCE-v2
16 claims resolved over 73 hashed files

Every public security claim names its enforcement path, positive and negative vectors, language coverage, formal status or explicit gap, assumptions, exclusions, and evidence artifact hash.

05

Portable implementation behavior

Shared vectors + evaluator-controlled rebuild
193 vectors plus 359 external hostility cases

The three reference ports are honestly labeled same-team consistency evidence. A separately authored Rust verifier is pinned to exact public source and tested against the current vector set; strict construction attestation remains separately disclosed.

06

Stateful enforcement under faults

Generated schedules + concurrent reservation storms
5,000 generated schedules and a 100-way reservation race

The durable gate checks at-most-once effects across concurrent workers, process restarts, abandoned reservations, stale-replica promotion, rollback attempts, and ambiguous executor outcomes.

Executable claim inventory

Every headline resolves to code, vectors, scope, and assumptions.

These are the current machine-verifiable claim statements. The JSON security case contains the exact enforcement paths and evidence hashes behind each one.

class-a-downgrade-refusedformal: partial

A receipt cannot turn a relying-party-pinned Class-A approver key into a bare Class-B signature path by self-declaring a weaker key class.

quorum-separation-of-dutiesformal: verified

A quorum cannot count the initiator as an approver or let one device key fill two approval seats.

scoped-authority-is-pinnedformal: partial

An authority proof is accepted only under a relying-party-pinned registry issuer and only within its action, role, policy, time, currency, amount, organization, and delegation scope.

reliance-requires-pinned-profileformal: partial

A cryptographically valid packet still refuses reliance unless signed action material satisfies the relying party's pinned assurance, organization-bound authority, exact registry head and epoch floor, policy, revocation, issuer, and consumption profile.

revocation-is-pinned-and-freshformal: not modeled

Revocation state is accepted only under a pinned revoker key, for the exact target, and within the relying party's freshness window.

timestamp-proof-requires-pinned-tsaformal: not modeled

A timestamp token carries weight only when its imprint binds the expected receipt digest and its signer matches a relying-party-pinned TSA key.

evidence-challenge-is-durably-registered-and-consumedformal: partial

An AE-CHALLENGE binds the canonical action and governing policy, is exposed only after atomic durable registration of its exact body, and is consumed on the first valid evaluation attempt across workers and restarts.

durable-consumption-is-owner-fencedformal: verified

Across concurrent workers and process restarts, one receipt has at most one active reservation, and only its opaque owner token can commit or release it.

ambiguous-effect-is-never-auto-retriedformal: partial

After an external executor is invoked, an exception is treated as an indeterminate effect and the approval is consumed or frozen rather than made reusable.

aec-execution-is-action-keyed-and-fleet-fail-closedformal: partial

The stateful AEC execution gate pins custom component verifiers, verifier keys, human profiles, and the requirement at construction, captures the validated store and logger methods, and refuses transaction-scoped trust configuration. It reserves one non-expiring key derived only from the executor-bound canonical action digest before effect, so presenter-controlled decoy components, alternate proof forms, or post-construction method replacement cannot mint a fresh replay key for the same action. Production construction also requires an ownership-fenced durable consumption backend and a strict atomic shared-head evidence log that continues across replicas and restarts; the gate independently rehashes and exactly matches each acknowledgment, and successful atomic append readback must equal the submitted sequence, predecessor, identifier, and content.

rx-sidecar-minimizes-patient-dataformal: not modeled

Rx evidence artifacts reject unknown or direct patient and clinical fields, use pairwise patient references and keyed source-record commitments, export a projection rather than recursively copying the transaction, and disclose it only under a pinned audience, purpose, policy, retention, artifact, and key-scope profile.

verify-package-is-byte-reproducibleformal: not modeled

The verify SDK canonicalizes package file modes, packs twice to byte-identical tarballs, and the publish workflow attests and publishes that exact tarball before comparing the registry copy byte-for-byte.

python-release-artifacts-are-byte-reproducibleformal: not modeled

The Python verifier builds its wheel and source distribution twice under a pinned source epoch, attests and publishes those exact bytes, and refuses a downloaded PyPI wheel or source distribution whose bytes differ.

all-package-releases-use-verifiable-bytesformal: not modeled

Every declared npm and PyPI package release requires a version-bound owner dispatch and protected-environment approval or explicit recorded administrator bypass, tests source from an immutable tag on main, constructs reproducible package bytes, attests the exact artifact plus security and conformance manifests, publishes through OIDC, and compares every registry artifact byte-for-byte after publication.

model-to-matter-clearance-is-exact-and-single-useformal: not modeled

A Model-to-Matter presentation clears at most once only when all six evidence types verify under the executor's constructor-pinned profile, bind the same exact digest-only action, satisfy freshness and the pinned revocation provider, and survive durable challenge and action consumption. The production executor refuses transaction-scoped profile, store, revocation, time, and retry configuration and captures validated state methods against post-construction replacement.

aec-role-substitution-refusedformal: not modeled

EP-AEC returns allow only when the relying party independently pins both its requirement and the exact executor action. Presenter labels are non-authoritative. The ep-receipt human leg requires a fresh Section 6.2 Trust Receipt with Class-A WebAuthn, a pinned approver directory, RP audience, signed WebAuthn origin allowlist, policy hash, and log key; a bare operator-signed envelope is refused. The ep-quorum leg requires a fresh exact pinned policy plus RP audience, signed WebAuthn origin allowlist, context policy, and key-to-identity-to-role directory. These predicates execute identically in JavaScript, Python, and Go.

Run it yourself

The review path is one command at a time.

npm run check:security-case
npm run conformance
npm run check:proof-stats
npm run check:llm-context
Boundaries

What this evidence does not establish.

The formal models do not prove that an AI model behaves well or that an approved action is wise, legal, or safe.

The symbolic model assumes perfect cryptography and authentic pinned roots; it does not model WebAuthn internals, parser correctness, clock arithmetic, collusion, or registry completeness.

JavaScript, Python, and Go are same-team ports. Their agreement demonstrates consistency, not independent construction.

The external Rust run is pinned interoperability evidence. Strict clean-room construction acceptance remains false until separately attested under an independently pinned key.

Complete mediation exists only when every protected path reaches the verifier at the actual system of record or actuator.

The shortest honest verdict

The architecture is the proposal. The executable security case is the evidence.

Read the assumptions, run the vectors, inspect the attack traces, and decide from the artifacts rather than from our adjectives.

Try to break the gateInspect Tamarin source
Engineering Evidence — Machine-Verifiable Security Case | EMILIA Protocol