The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning. Learn more →
Top 17 model-checking Open-Source Projects
-
-
tlaplus
TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
-
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.
-
-
-
BlockingQueue
Tutorial "Weeks of debugging can save you hours of TLA+". Each git commit introduces a new concept => check the git history! (by lemmy)
-
-
WorkOS
The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.
-
-
-
-
-
SMPT
SMPT is a SMT-based model checker for Petri nets focused on reachability problems that takes advantage of net reductions (polyhedral reductions).
-
SaaSHub
SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives
Project mention: Ask HN: Usefulness of formal verification (Coq) and formal verification (TLA+)? | news.ycombinator.com | 2024-04-07
4. SQA wiki
Project mention: The C Bounded Model Checker: Criminally Underused | news.ycombinator.com | 2024-01-30This is also the backend for Kani - Amazon's formal verification tool for Rust.
https://github.com/model-checking/kani
Project mention: Basic SAT model of x86 instructions using Z3, autogenerated from Intel docs | news.ycombinator.com | 2023-05-15You can use it to (mostly) validate small snippets are the same. See Alive2 for the application of Z3/formalization of programs as SMT for that [1]. As far as I'm aware there are some problems scaling up to arbitrarily sized programs due to a lack of formalization in higher level languages in addition to computational constraints. With a lot of time and effort it can be done though [2].
1. https://github.com/AliveToolkit/alive2
2. https://sel4.systems/
I also found https://github.com/nicolasAmat/SMPT maybe it should be used because SMT, Z3 looks familiar. It's used in fancy new theorem provers.
And a project uses it to check for deadlocks. https://github.com/hlisdero/cargo-check-deadlock/ but it doesn't work for async code, yet.
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).
model-checking related posts
- Ask HN: Usefulness of formal verification (Coq) and formal verification (TLA+)?
- The C Bounded Model Checker: Criminally Underused
- Holiday protocols: secret Santa with Quint
- Quint: A specification language based on the temporal logic of actions (TLA)
- The Wizardry Frontier
- Kani 0.40.0 has been released!
- Kani 0.39.0 has been released!
-
A note from our sponsor - WorkOS
workos.com | 24 Apr 2024
Index
What are some of the best open-source model-checking projects? This list will help you:
| Project | Stars | |
|---|---|---|
| 1 | P | 2,911 |
| 2 | tlaplus | 2,201 |
| 3 | sqa-wiki | 2,200 |
| 4 | kani | 1,885 |
| 5 | alive2 | 675 |
| 6 | BlockingQueue | 480 |
| 7 | apalache | 409 |
| 8 | vscode-tlaplus | 329 |
| 9 | ewd998 | 46 |
| 10 | smcdel | 39 |
| 11 | tla-web | 37 |
| 12 | modelator-py | 28 |
| 13 | SMPT | 27 |
| 14 | cargo-check-deadlock | 17 |
| 15 | tlsd | 12 |
| 16 | lincheck | 8 |
| 17 | smanikin | 2 |
Sponsored
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com