Specifications and observable evidence
Make correctness inspectable.
A specification defines the intended behavior. Machine checks examine bounded designs and observed executions. Each verdict has a scope, a configuration and an exact set of inputs.
Specify the failures first
Each phase defines state, actions, invariants, bounds and environmental assumptions in TLA+. TLC explores finite configurations. Separate liveness checks state their fairness and recovery assumptions.
Deliberately faulty variants test whether the checks detect intended violations. Reachability witnesses help expose specifications that appear safe only because useful behavior is unreachable.
Check what the implementation actually did
The implementation workflow requires observations at real state, durability and reply boundaries, checked against independent specification predicates. The mapping must connect requirements, model transitions, source behavior and run evidence in both directions.
Trace conformance must validate the initial state, continuity and each allowed abstract transition, including refusals, retries and recovery. Native Mira execution conformance and source-level refinement have not been established.
A verdict is only as broad as its evidence
Passing bounded TLC checks is not a proof over every possible system size. A conforming execution trace is evidence about that execution under its abstraction, not a proof about every possible implementation execution.
Deterministic simulation of production components, independent histories, fuzzing, real I/O and adversarial campaigns add different evidence. The formal suite and its overall verification are still incomplete.
Close a phase on recorded output
Acceptance pins sources, tools, configuration and reports. The entire foundation must meet its acceptance obligations before resource implementation begins. The full resource model then needs whole-system evidence before the database is complete.
Missing checks, timeouts, stale reports and truncated traces do not count as success. Human review still decides whether the modeled requirements are the intended product.
Help shape what comes next.
Talk to the founder