My TLA+ specifications, mostly written in Pluscal.
- 2-phase commit: https://github.com/FedericoPonzi/tla-plus-specs/tree/main/2-phase-commit
- 3-phase commit: https://github.com/FedericoPonzi/tla-plus-specs/tree/main/3-phase-commit
- An incorrect way to model a lease algorithm: https://github.com/FedericoPonzi/tla-plus-specs/tree/main/lease-buggy-code
- Lamport Clock used to solve mutual exclusion problem: logical-clocks-and-mutual-exclusion
- Modeling of the solution for the problem of Missionaries and Cannibals: https://github.com/FedericoPonzi/tla-plus-specs/tree/main/missionaries_and_cannibals_problem
- I've started watching this talk "Weeks of debugging can save you hours of TLA+", and thought it would be fun to stop it and try to find the bug myself in tla+: https://github.com/FedericoPonzi/tla-plus-specs/tree/main/weeks_of_debugging
- Wolf, Goat and Cabbage is similar to the Missionaries and cannibals problem. A fun exercise to improve my tla+: https://github.com/FedericoPonzi/tla-plus-specs/tree/main/wolf_goat_cabbage
- Chandy-lamport distributed snapshots algorithm: https://github.com/FedericoPonzi/tla-plus-specs/tree/main/chandy-lamport-distributed-snapshots
I've also written some blog posts on TLA+: