awesome-rust-formalized-reasoning
minisat
Our great sponsors
| awesome-rust-formalized-reasoning | minisat | |
|---|---|---|
| 3 | 0 | |
| 227 | 1 | |
| - | - | |
| 0.0 | 0.0 | |
| 5 days ago | over 2 years ago | |
| MIT License | BSD 3-clause "New" or "Revised" License |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
awesome-rust-formalized-reasoning
-
CreuSAT: Formally verified SAT solver written in Rust and verified with Creusot
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.
-
Kani Rust Verifier – a bit-precise model-checker for Rust
This dispersed progress is the sign of an absence of maturity but the exploration of this space with Rust is very promising : https://github.com/newca12/awesome-rust-formalized-reasoning
minisat
We haven't tracked posts mentioning minisat yet.
Tracking mentions began in Dec 2020.
What are some alternatives?
picosat - Haskell bindings for PicoSAT solver
tamarin-prover - Main source code repository of the Tamarin prover for security protocol verification.
kani - Kani Rust Verifier
hatt - Truth-table generator for classical propositional logic
atp-haskell - Haskell version of the code from "Handbook of Practical Logic and Automated Reasoning"
qed - Experiments writing a prover
satchmo - SAT encoder
Kind - A next-gen functional language [Moved to: https://github.com/Kindelia/Kind2]
obdd - pure Haskell implementation of reduced ordered binary decision diagrams
judge - Tableau-based theorem prover for justification logic.
structural-induction - SII: Structural Induction Instantiator over any strictly-positive algebraic data type.
Formality - A modern proof language [Moved to: https://github.com/kind-lang/Kind]