Sovereign ERPA ledger and period-close kernel whose rules are checked by model checking and formal specifications.Status: Walking skeleton: period controller and ledger port, model-checked

Period close as a checked state machine. The Period Controller decides close, reopen and adjustment moves, and its invariants are checked against a TLA+ specification in lockstep.

An engine-neutral ledger. A Ledger Port interface with a conformance suite that any ledger engine adapter has to pass.

Seeded defects are caught. Deliberately broken variants are run against the checks, and each one is caught with its shortest counterexample.

Check it yourself: Run the workspace tests and read the counts: the controller and the TLA+ transcription agree on every reachable state, and each seeded defect is caught with its shortest counterexample.