paralin/tla

Use when writing or changing code that holds state across steps (a lifecycle, a lock, a queue, a protocol, a cache, storage, a retry, a screen's states), when a defect needs an interleaving, a restart or a crash to happen, or when simplifying such code. Models the whole program in TLA+, with each spec in a .tla file beside the code it describes, checks the specs with tla-ts, and uses the model and the code together to make both simpler.