26
TLA+ state-machine invariants
TLC 2.19; no reported error in the checked configuration
EMILIA / verification status
The proof surface is public.
This page reports the latest machine-generated evidence snapshot. It exposes the numbers, the retained attack traces, and the boundary between what was checked and what was not.
This is not a production security clearance. The current Strix retest and deployment validation remain open until the fixes are deployed and re-tested on the live service.
Current status
Repository checks passed
Generated 2026-08-24T15:57:00.110Z
35 / 32
Alloy structural checks
facts / assertions in the current model inventory
20
Tamarin symbolic obligations
8 deliberately unsafe counterexamples retained
35
Executable security claims
259 hashed evidence files in the resolved case
332
Conformance vectors
21 suites across 3 reference ports
10,013
Automated test cases
620 test files; platform-specific skips are disclosed
How to read this
Evidence is layered, not averaged.
The symbolic models constrain protocol state. Executable claims connect those constraints to code and vectors. Conformance checks portability. Stateful fault tests exercise the path under races and restarts. No one layer gets to borrow another layer’s authority.
Claim boundary
What this does not establish.
This is a repository evidence snapshot, not an assertion that every deployed instance has been independently verified.
Formal results apply only within each model’s stated assumptions and bounded configuration.
The external implementation evidence is interoperability evidence; strict clean-room acceptance remains separately disclosed.
A passing model or test does not prove that an approved action is wise, legal, or safe.