Ingest, store, & analyze all types of time series data in a fully-managed, purpose-built database. Keep data forever with low-cost storage and superior data compression. Learn more →
Top 23 Formal Method Open-Source Projects
-
Project mention: Best local database that works on all platforms including web? | reddit.com/r/FlutterDev | 2023-03-02
Have you looked into other pure-Rust databases as well, such as sled or GlueSQL which has an SQL interface on top of sled? I wonder how those would compare to Persy.
-
Project mention: Algebra Rules: The Most Useful Rules of Basic Algebra | reddit.com/r/InternetIsBeautiful | 2023-02-04
Anyone who is interested in this might also be interested in Lean.
-
SonarLint
Clean code begins in your IDE with SonarLint. Up your coding game and discover issues early. SonarLint is a free plugin that helps you find & fix bugs and security issues from the moment you start writing code. Install from your favorite IDE marketplace today.
-
Project mention: One step forward, an easier interoperability between Rust and Haskell | IOG Engineering | reddit.com/r/haskell | 2023-01-27
Nice work. About cryptonite: have IOG considered using crypto primitives provided by HACL*/evercrypt?
-
magmide
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
Project mention: Announcing Magmide Month! (proof language for/using Rust) | reddit.com/r/rust | 2023-02-28 -
creusot
deductive verification of Rust code. (semi) automatically prove your code satisfies your specifications!
Project mention: Prop v0.42 released! Don't panic! The answer is... support for dependent types :) | reddit.com/r/rust | 2023-01-18Wow that sounds really cool! I'm not an expert but does that mean that one day you could implement dependend types or refinement types in Rust as a crate ? I currently only know of tools like: Flux Creusot Kani Prusti
-
Project mention: CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot | reddit.com/r/u_Dazzling_Finger_8120 | 2022-06-18
-
Project mention: We Need Simpler Types (speculations on what can be improved in future type systems and on erasing the boundaries between types and values) | reddit.com/r/ProgrammingLanguages | 2022-09-14
https://github.com/ligurio/practical-fm Look for Coq, Agda, Idris, MS - F*.
-
InfluxDB
Access the most powerful time series database as a service. Ingest, store, & analyze all types of time series data in a fully-managed, purpose-built database. Keep data forever with low-cost storage and superior data compression.
-
Project mention: Design by contract - Preconditions and Postconditions - I'm really amazed with Scala. | reddit.com/r/scala | 2023-03-02
You may find Dtainless interesting.
-
Project mention: First article of a series about Recife (Clojure model checker on top of TLA+ tooling) | reddit.com/r/Clojure | 2023-02-19
😁 thanks! At least now the TLA+ maintainer itself is recommending https://github.com/tlaplus/vscode-tlaplus, an improvement.
-
spark-by-example
SPARK by Example is an adaptation of ACSL by Example for SPARK 2014, a programming language which is a formally verified subset of Ada
Project mention: Spark by Example is an adaptation of ACSL by Example for SPARK 2014, a programm | news.ycombinator.com | 2022-11-18 -
-
-
Project mention: Let's collect relatively new research programming languages in this thread | reddit.com/r/ProgrammingLanguages | 2022-11-15
https://github.com/koka-lang/koka Algebraic effects and reference counting. https://github.com/mit-plv/koika hardware description DSL for coq
-
-
RecordFlux
Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
-
-
-
-
-
-
-
-
-
SaaSHub
SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives
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).
The latest post mention was on 2023-03-02.
Formal Methods related posts
- Announcing Magmide Month! (proof language for/using Rust)
- Algebra Rules: The Most Useful Rules of Basic Algebra
- One step forward, an easier interoperability between Rust and Haskell | IOG Engineering
- Lean – Theorem Prover
- Thoughts on proof assistants?
- Spark by Example is an adaptation of ACSL by Example for SPARK 2014, a programm
- SPARK Ada by Example
-
A note from our sponsor - InfluxDB
www.influxdata.com | 28 Mar 2023
Index
What are some of the best open-source Formal Method projects? This list will help you:
| Project | Stars | |
|---|---|---|
| 1 | sled | 6,800 |
| 2 | mathlib | 1,465 |
| 3 | hacl-star | 1,463 |
| 4 | magmide | 750 |
| 5 | creusot | 646 |
| 6 | CreuSAT | 507 |
| 7 | practical-fm | 412 |
| 8 | stainless | 315 |
| 9 | vscode-tlaplus | 272 |
| 10 | spark-by-example | 145 |
| 11 | what4 | 135 |
| 12 | z3_tutorial | 131 |
| 13 | koika | 102 |
| 14 | miss_hit | 100 |
| 15 | RecordFlux | 92 |
| 16 | acsl-by-example | 87 |
| 17 | hermit | 48 |
| 18 | sbvPlugin | 40 |
| 19 | hardware | 18 |
| 20 | smtlib2 | 14 |
| 21 | AttackerSynthesis | 12 |
| 22 | timewinder | 11 |
| 23 | afv | 9 |
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com