Authored inventory / Work in progress
125TLA+ modules
Authored foundation, resource and composed-system models.
Project snapshot · 13 September 2026
Formal models written. Engine work ahead.
The current TLA+ suite covers the foundation and resource design. Some bounded checks have passed, but the formal package is incomplete and the Mira engine has not yet been implemented.
Authored inventory / Work in progress
161Model configurations
Authored configurations for finite model-checking scenarios.
Snapshot: 13 September 2026. These are file counts, not passing-check counts. Formal verification is incomplete; implementation conformance and release qualification remain pending.
Foundation research and formal models
The foundation adoption plan is based on a pinned TigerBeetle source checkout. The authored models cover foundation behavior, individual resource rules and their system-level composition.
These source files are an inventory of work in progress. Their number does not establish completeness, correctness or implementation readiness.
Verification remains open
The evidence includes bounded TLC runs, negative controls and reachability witnesses. Other checks have timed out or become stale as models changed. Supplemental results are not yet fully consolidated into the central evidence registry.
Composition, native ABI and cryptographic obligations, and the connection from specifications to actual source behavior still need completion. No whole-system proof or implementation-conformance certificate is claimed.
What remains before a release
Complete and verify the inherited foundation, then implement and qualify the full resource model with its clients, security and operations. Both database phases must close before enterprise implementation begins.
There is no qualified Mira production binary, public throughput result or production SDK release in this snapshot.
Help shape what comes next.
Talk to the founder