We have a number of TLA+ models at Oxide. Here's one:

https://github.com/oxidecomputer/omicron/blob/8b0886dbd02229...