A TLA+ formal model of a laptop’s power states and transitions. Specifies and verifies the correctness of state changes between power modes.

The TLA+ specification can be found on GitHub: https://github.com/EricSpencer00/tla-laptop