tlaplus

Top 17 tlaplu Open-Source Projects

  • Examples

    A collection of TLA⁺ specifications of varying complexities (by tlaplus)

  • Project mention: Suggestions for model checking? | /r/tlaplus | 2023-07-12

    I need to write a small case study using TLA+. Where can I find some distributed/concurrent algorithm or system that is not too complex and hasn't been specified yet? There are so many examples already covered in the official repository alone that I'm out of ideas.

  • InfluxDB

    Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.

    InfluxDB logo
  • DrTLAPlus

    Dr. TLA+ series - learn an algorithm and protocol, study a specification

  • quint

    An executable specification language with delightful tooling based on the temporal logic of actions (TLA) (by informalsystems)

  • Project mention: Holiday protocols: secret Santa with Quint | news.ycombinator.com | 2023-12-21

    Hi! I wrote a blogpost exploring a formal specification in Quint [1] for the secret santa game, and verifying some of its properties with Apalache [2].

    Hope you enjoy it, and any feedback is welcome. Happy holidays!

    [1]: https://github.com/informalsystems/quint

  • BlockingQueue

    Tutorial "Weeks of debugging can save you hours of TLA+". Each git commit introduces a new concept => check the git history! (by lemmy)

  • practical-fm

    A gently curated list of companies using verification formal methods in industry

  • apalache

    APALACHE: symbolic model checker for TLA+ and Quint

  • Project mention: Verified Rust for low-level systems code | news.ycombinator.com | 2024-05-04

    TLA+ has also had an SMT-based backend, Apalache [1], for a few years now. In general, you encode your system model (which would be the Rust functions for Verus, the TLA model for Apalache) and your desired properties into an SMT formula, and you let the solver have a go at it. The deal is that the SMT language is quite expressive, which makes such encodings... not easy, but not impossible. And after you're done with it, you can leverage all the existing solvers that people have built.

    While there is a series of "standard" techniques for encoding particular program languages features into SMT (e.g., handling higher-order functions, which SMT solves don't handle natively), the details of how you encode the model/properties are extremely specific to each formalism, and you need to be very careful to ensure that the encoding is sound. You'd need to go and read the relevant papers to see how this is done.

    [1]: https://apalache.informal.systems

  • CommunityModules

    TLA+ snippets, operators, and modules contributed and curated by the TLA+ community

  • SaaSHub

    SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives

    SaaSHub logo
  • tlaplus-graph-explorer

    A static web application to explore and animate a TLA+ state graph.

  • fizzbee

    Easiest-ever formal methods language! Designed for developers crafting distributed systems, microservices, and cloud applications

  • Project mention: FizzBee: Open-source formal methods tool that's not hard | news.ycombinator.com | 2024-04-01
  • tla-web

    Interactive, web-based environment for exploring TLA+ specifications.

  • tree-sitter-tlaplus

    A tree-sitter grammar for TLA⁺ and PlusCal

  • ewd998

    Distributed termination detection on a ring, due to Shmuel Safra:

  • modelator-py

    Utilities for the TLA+ ecoystem and model-based testing using TLA+.

  • TLAplus

    TLA+ questions, answers, and experiments (by Isaac-DeFrain)

  • tlsd

    Generate (message) sequence diagrams from TLA+ state traces

  • advent-of-tla

    AoC goals in TLA+

  • timewinder

    Temporal Logic of Actions in Rust via Starlark

  • SaaSHub

    SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives

    SaaSHub logo
NOTE: The open source projects on this list are ordered by number of github stars. The number of mentions indicates repo mentiontions in the last 12 Months or since we started tracking (Dec 2020).

tlaplus discussion

Log in or Post with

tlaplus related posts

  • Verified Rust for low-level systems code

    6 projects | news.ycombinator.com | 4 May 2024
  • Holiday protocols: secret Santa with Quint

    3 projects | news.ycombinator.com | 21 Dec 2023
  • Quint: A specification language based on the temporal logic of actions (TLA)

    5 projects | news.ycombinator.com | 19 Dec 2023
  • Suggestions for model checking?

    1 project | /r/tlaplus | 12 Jul 2023
  • Quint – a new language based on TLA+ with modern syntax and developer tooling

    1 project | news.ycombinator.com | 9 Jul 2023
  • How to specify "After P is true, Q is always true"?

    1 project | /r/tlaplus | 30 Mar 2023
  • Writing a TLA⁺ tree-sitter grammar: my foray into free software

    2 projects | news.ycombinator.com | 12 Jan 2023
  • A note from our sponsor - InfluxDB
    www.influxdata.com | 16 Jun 2024
    Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality. Learn more →

Index

What are some of the best open-source tlaplu projects? This list will help you:

Project Stars
1 Examples 1,240
2 DrTLAPlus 777
3 quint 600
4 BlockingQueue 482
5 practical-fm 470
6 apalache 414
7 CommunityModules 262
8 tlaplus-graph-explorer 195
9 fizzbee 89
10 tla-web 63
11 tree-sitter-tlaplus 54
12 ewd998 46
13 modelator-py 28
14 TLAplus 22
15 tlsd 12
16 advent-of-tla 7
17 timewinder 0

Sponsored
Power Real-Time Data Analytics at Scale
Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
www.influxdata.com