Sonar helps you commit clean code every time. With over 600 unique rules to find Java bugs, code smells & vulnerabilities, Sonar finds the issues while you focus on the work. Learn more →
Top 23 Formal Verification Open-Source Projects
-
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?
-
Efforts: seL4, Project Everest, the Prossimo project of the ISRG, Let's Encrypt, and Prusti for the Rust language
-
Sonar
Write Clean Java Code. Always.. Sonar helps you commit clean code every time. With over 600 unique rules to find Java bugs, code smells & vulnerabilities, Sonar finds the issues while you focus on the work.
-
Project mention: Don’t call it a comeback: Why Java is still champ | news.ycombinator.com | 2022-08-09
Java should adopt something like the Checker Framework Nullness Checker in its first-party tooling.
-
Project mention: Tools for Verifying a Language and its Semantics | reddit.com/r/ProgrammingLanguages | 2023-01-02
You may want to look at [CakeML](https://cakeml.org) done in HOL4, there is also a nice proof pearl about a more .. minimalistic verified bootstrapped compiler also in HOL4.
-
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
-
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: 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*.
-
Personally I treat Coq like an extension of my brain. Whenever I'm uncertain about something, I formalize it in Coq. I have a repository of proofs with GitHub Actions set up in such a way forbids me from pushing commits containing mathematical mistakes. I've formalized various aspects of category theory, type theory, domain theory, etc., and I've also verified a few programs, such as this sorting algorithm. Lately I've been experimenting with a few novel types of graphs, proving various properties about them with the aim of eventually developing a way to organize all of my data (files, notes, photos, passwords, etc.) in some kind of graph structure like that.
-
awesome-rust-formalized-reasoning
An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.
Project mention: CreuSAT: Formally verified SAT solver written in Rust and verified with Creusot | news.ycombinator.com | 2022-06-17Unsurprisingly, we can see a growing interest in the Rust ecosystem regarding formal verification. I try to keep https://github.com/newca12/awesome-rust-formalized-reasoning up to date. I will add CreuSAT shortly.
-
-
-
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 -
OpenJML
This is the primary repository for the source code of the OpenJML project. The source code is licensed under GPLv2 because it derives from OpenJDK which is so licensed. The active issues list for OpenJML development is here and the wiki contains information relevant to development. Public documentation for users is at the project website:
Project mention: Anybody tried OpenJML's static checker? What's it's state? | reddit.com/r/java | 2022-04-29Has anyone successfully used OpenJML's static checker on a real project to reduce defects?
-
RecordFlux
Formal specification and generation of verifiable binary parsers, message generators and protocol state machines
Project mention: Why isn't there a Swagger/OpenAPI for binary formats? | news.ycombinator.com | 2022-03-25 -
-
-
-
-
-
-
As a real world example you can take a look at the Image_Ranged and Image_Modular functions defined in basalt-strings_generic.ads and basalt-strings_generic.adb. The goal property for these functions is (apart from the absence of runtime errors) that they always return a string that starts at the index 1 and that has a specific maximum length, depending on the base given.
-
isabelle-lambda-calculus
A formal definition and verification of System F. To be extended to System Fc
-
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-02-28.
Formal Verification related posts
- Announcing Magmide Month! (proof language for/using Rust)
- Prop v0.42 released! Don't panic! The answer is... support for dependent types :)
- Tools for Verifying a Language and its Semantics
- Spark by Example is an adaptation of ACSL by Example for SPARK 2014, a programm
- SPARK Ada by Example
- Prusti: Static Analyzer for Rust
- Prusti: Static Analyzer for Rust
-
A note from our sponsor - Sonar
www.sonarsource.com | 22 Mar 2023
Index
What are some of the best open-source Formal Verification projects? This list will help you:
| Project | Stars | |
|---|---|---|
| 1 | hacl-star | 1,463 |
| 2 | prusti-dev | 1,234 |
| 3 | Checker Framework | 897 |
| 4 | cakeml | 799 |
| 5 | magmide | 749 |
| 6 | creusot | 644 |
| 7 | CreuSAT | 506 |
| 8 | practical-fm | 412 |
| 9 | proofs | 240 |
| 10 | awesome-rust-formalized-reasoning | 196 |
| 11 | hacspec | 181 |
| 12 | Daikon | 163 |
| 13 | spark-by-example | 145 |
| 14 | OpenJML | 114 |
| 15 | RecordFlux | 92 |
| 16 | CATG | 90 |
| 17 | acsl-by-example | 87 |
| 18 | jCUTE | 81 |
| 19 | libsparkcrypto | 26 |
| 20 | hardware | 18 |
| 21 | TLAplus | 16 |
| 22 | basalt | 9 |
| 23 | isabelle-lambda-calculus | 8 |
SaaSHub - Software Alternatives and Reviews
SaaSHub helps you find the best software and product alternatives
www.saashub.com