Machines and proofs
Lifecycles declared as data and checked for every possible run
Tests check the runs someone thought of. For code that moves money, that is not enough. These pages show how a lifecycle becomes a table the production code reads, how tests sweep every cell of that table, and how a model checker proves the safety rules hold for runs of any length.
-
State machines as data
Declare the lifecycle once, sweep every cell, derive everything else
-
TLA+ models checked by Apalache
Prove the safety rules hold for runs of any length, using the real transitions