Hacker GitHub

← All repos

tlaplus/Examples

View on GitHub ↗ ★ 1,603 TLA

A collection of TLA⁺ specifications of varying complexities.

8 mentions on Hacker News by 7 people: 0 stories, 8 comments · first 2017-01-17 · latest 2026-07-31

Mentions per year 8 mentions · busiest year 2017 (3)
20082026
AllStoriesComments NewestTopOldest
  1. Simulating Elevators in TLA+ is a fun exercise. https://github.com/tlaplus/Examples/blob/master/specificatio... Another interesting, and underrated one: hotel keys.
    comment by agentultra · 2026-07-31 · in Show HN: Elevators
  2. …and tools[3] Thanks for the link, _doctor_love [1] https://lamport.azurewebsites.net/ [2] https://github.com/tlaplus/Examples [3] https://github.com/tlaplus/tlaplus/
    comment by schaefer · 2026-05-09 · in Can LLMs model real-world systems in TLA+?
  3. Hillel Wayne's "Practical TLA+" book and the TLA+ examples repository ( https://github.com/tlaplus/Examples ) both contain excellent worked examples ranging from simple algorithms to complex distributed systems.
    comment by ethan_smith · 2025-07-28 · in Formal specs as sets of behaviors
  4. The TLA Plus examples repository is very good: https://github.com/tlaplus/Examples . I would recommend starting with something simple like the DieHard problem.
    comment by teeray · 2025-05-30 · in Systems Correctness Practices at Amazon Web Services
  5. …Lamport's (very charming) video tutorials at OP's link and studied some of the specifications at https://github.com/tlaplus/Examples/tree/master/specificatio... I'm less sure now that I can. I'll keep plugging away, but if anyone here has…
    comment by gralx · 2019-05-03 · in TLA+: design, model, document, and verify concurrent systems
  6. …https://www.linkedin.com/pulse/lamports-tla-spec-testing-why... https://github.com/tlaplus/Examples/tree/master/specificatio... https://github.com/tlaplus/Examples/tree/master/specificatio...
    comment by pron · 2017-06-15 · in TLA+ in Practice and Theory, Part 4: Order in TLA+
  7. …I personally cut my teeth on a river-crossing puzzle with a farmer, wolf, and sheep. [0] https://github.com/tlaplus/Examples/tree/master/specificatio... [1] https://www.youtube.com/watch?v=6cAbgAaEOVE [2]…
    comment by ahelwer · 2017-03-21 · in Leslie Lamport: Video course on TLA+
  8. Paxos-based means what exactly? How much of the specification does it implement? [0] [0] https://github.com/tlaplus/Examples/tree/master/specificatio...
    comment by agentultra · 2017-01-17 · in A Paxos-based Redis replication layer with dynamic reconfiguration in 500 lines