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
HACL*, a formally verified cryptographic library written in F*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?
A static verifier for Rust, based on the Viper verification infrastructure.Project mention: A plan for cybersecurity and grid safety | dev.to | 2023-02-10
Efforts: seL4, Project Everest, the Prossimo project of the ISRG, Let's Encrypt, and Prusti for the Rust language
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.
Pluggable type-checking for JavaProject 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.
CakeML: A Verified Implementation of MLProject 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.
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
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-18
Wow 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
CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.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
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.
A gently curated list of companies using verification formal methods in industryProject 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*.
My personal repository of formally verified mathematics.Project mention: Thoughts on proof assistants? | reddit.com/r/ProgrammingLanguages | 2022-12-13
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.
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-17
Unsurprisingly, 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.
A specification language for cryptography primitives.
Dynamic detection of likely invariants
SPARK by Example is an adaptation of ACSL by Example for SPARK 2014, a programming language which is a formally verified subset of AdaProject mention: Spark by Example is an adaptation of ACSL by Example for SPARK 2014, a programm | news.ycombinator.com | 2022-11-18
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-29
Has anyone successfully used OpenJML's static checker on a real project to reduce defects?
Formal specification and generation of verifiable binary parsers, message generators and protocol state machinesProject mention: Why isn't there a Swagger/OpenAPI for binary formats? | news.ycombinator.com | 2022-03-25
a concolic testing engine for Java
Public snapshots of "ACSL by Example"
Java Concolic Unit Testing Engine
A cryptographic library in SPARK 2014
Verilog development and verification project for HOL4 (by CakeML)
TLA+ questions, answers, and experiments (by Isaac-DeFrain)
Collection of formally verified building blocks (by Componolit)Project mention: SPARK Guide | reddit.com/r/ada | 2022-06-10
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.
A formal definition and verification of System F. To be extended to System Fc
SaaSHub - Software Alternatives and Reviews. SaaSHub helps you find the best software and product alternatives
Formal Verification related posts
Announcing Magmide Month! (proof language for/using Rust)
1 project | reddit.com/r/rust | 28 Feb 2023
Prop v0.42 released! Don't panic! The answer is... support for dependent types :)
5 projects | reddit.com/r/rust | 18 Jan 2023
Tools for Verifying a Language and its Semantics
1 project | reddit.com/r/ProgrammingLanguages | 2 Jan 2023
Spark by Example is an adaptation of ACSL by Example for SPARK 2014, a programm
1 project | news.ycombinator.com | 18 Nov 2022
SPARK Ada by Example
1 project | news.ycombinator.com | 7 Nov 2022
Prusti: Static Analyzer for Rust
1 project | reddit.com/r/patient_hackernews | 13 Oct 2022
Prusti: Static Analyzer for Rust
1 project | reddit.com/r/hackernews | 13 Oct 2022
A note from our sponsor - Sonar
www.sonarsource.com | 22 Mar 2023
What are some of the best open-source Formal Verification projects? This list will help you: