Nine customer services over three entities: registering, opening an account,
deposits and withdrawals, transfers, salary runs, balances and closing an
account. It is the model to read first, and it is read the way the method
works, top down: a service’s requirements, then who is responsible for meeting
each of them, then how the work is orchestrated, and then the same again one
level down.
The model verifies with no errors at either verification level. It keeps five warnings, each with a written reason. They concern the ledger’s record of an entry, whose contents no contract states yet.
