An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.
As of May 29, 2022, proof of computation & cryptographic stuff are considered off-topic.
awesome-rust-formalized-reasoning is an EDLA project.
The purpose of edla.org is to promote the state of the art in various domains.
- Actively maintened π₯
- Archived π
- Benchmark β
- Best in Class
β¦οΈ - Book implementation π
- Crate(s) π¦
- Crates keyword fully listed π―
- Deleted by author β»οΈ
- Educational project π
- Exhumated π»
- Inactive π€
- List of resources βΉοΈ
- Popular β
- Research paper implementation π₯Ό
- Toy project π€
- Video πΊ
- WIP π§
- CoP π¦ - reimplement automated theorem provers of the leanCoP family, such as leanCoP and nanoCoP.
- lazyCoP βπ€ - automatic theorem prover for first-order logic with equality.
- lerna π - proves theorems.
- lickety - prototype system for linear resolution with splitting.
- meancop π¦β»οΈ - became CoP.
- Serkr βπ» - automated theorem prover for first order logic with equality.
- theorem-prover-rs - rewrite of theorem-prover-kt a sequent-style automated theorem prover.
- BatSat π¦β - solver forked from ratsat, a reimplementation of MiniSat.
- Colombini-SAT - simple 3-SAT solver.
- CreuSAT β - formally verified SAT solver verified with Creusot.
- Debug-SAT π¦ - debuggable automatic theorem prover for boolean satisfiability problems (SAT).
- dpll-sat π€ - naΓ―ve SAT solver implementing the classic DPLL algorithm.
- DRSAT - Daniel's Rusty SAT solver.
- lutrix π€ - SAT/SMT Solver.
- minisat-rust βπ€ - experimental minisat SAT solver.
- msat π¦π - MaxSAT Solver.
- RatSat π¦π¦βπ€ - reimplementation of MiniSat.
- Resolvo π¦β - fast package resolver (CDCL based SAT solving).
- rsat π¦π - SAT Solver.
- RsBDD - Reduced-order Binary Decision Diagram (RoBDD) SAT solver.
- rust-sat π€ - SAT solver that accepts input in the DIMACS CNF file format.
- rustsat π€ - toy SAT solver.
- sat - simple CDCL sat solver.
- SAT solver π€π€ - SAT solver.
- SAT-MICRO π₯Ό - reimplementation of the SAT-solver described in 'SAT-MICRO: petit mais costaud!'.
- sat-solver - simple CDCL SAT solver based on the lecture 185.A93 Formal Methods in CS at TU Wien.
- SATCoP π€ - theorem prover for first-order logic based on connection tableau and SAT solving.
- Satire π¦ π€ - educational SAT solver.
- satyrs ππ€ - DPLL SAT solver.
- scrapsat π€ - CDCDL SAT Solver.
- screwsat π¦β - simple CDCL SAT Solver.
- Scuttle π¦π¦ - multi-objective MaxSAT solver based on the rustsat library and the CaDiCaL SAT solver.
slpπ¦β»οΈ - became SolHOP.- SolHOP π¦π - aims to be a SAT and MaxSAT solver. Currently, a CDCL based SAT.
- Splr π¦
β¦οΈ β - modern CDCL SAT solver. - starlit π§ - CDCL SAT solver.
- Stevia βπ€ - simple (unfinished) SMT solver for QF_ABV.
- UASAT-RS - SAT solver based calculator for discrete mathematics and universal algebra.
- Varisatπ¦π¦π¦π¦π¦π¦π¦π¦β - CDCL based SAT solver.
- ellp π¦π§ - linear programming library that provides primal and dual simplex solvers.
- minilp π¦βπ - linear programming solver.
- hakim - hacky interactive theorem prover.
cobaltβ»οΈπ» - a wip minimal proof assistant.- Esther π€ - simple automated proof assistant.
- homotopy-rs
β¦οΈ βπ₯Όπ₯Όπ₯ - implementation of homotopy.io proof assistant. - LSTS π¦β - proof assistant that is also a programming language.
- Noq πΊβ - Not Coq. Simple expression transformer that is not Coq.
- Poi π¦β - pragmatic point-free theorem prover assistant.
- Proost - simple proof assistant.
- qbar π¦π€ - experimental automated theorem verifier/prover and proof assistant.
- Avalog π¦β - experimental implementation of Avatar Logic with a Prolog-like syntax.
- autosat π¦π€ - automatic conversion of functions to CNF for SAT solving.
- Caso π¦ - category Theory Solver for Commutative Diagrams.
- cyclegg - cyclic theorem prover for equational reasoning using egraph.
- good_lp β - Mixed Integer Linear Programming modeler using external solvers.
- gpp-solver π¦ - small hybrid push-pull solver/planner that has the best of both worlds.
- hoice β - ICE-based Constrained Horn Clause (CHC) solver.
- linear_solver π¦β - linear solver designed to be easy to use with Rust enums.
- Logic solver βπ€ - logic solver.
- Mikino π¦π¦ - simple induction and BMC engine.
- Monotonic-Solver π¦β - monotonic solver designed to be easy to use with Rust enum expressions.
- nnoq - simple theorem prover (nay, verifier) based on functional expression rewriting.
- nyaya - proof language based on sequent calculus and Metamath.
- Obvious π€ - simple little logic solver and calculator.
- pocket_prover π¦π¦β - fast, brute force, automatic theorem prover for first order logic.
- prover π - first-order logic prover.
- prover(2) π€π€ - experiment with integer relation prover.
- QED Prover βπ₯Ό - reimplementation of the Cosette prover in Rust.
- reachability_solver π¦ - linear reachability solver for directional edges.
- relsat-rs π€ - Experiments with provers.
- SAT-bench - benchmark suit for SAT solvers.
- sat_lab π€π§ - framework for manipulating SAT problems.
- SAT solver ANalyser π§ - toolbox for analyzing performance and runtime characteristics of SAT solvers.
- sequentprover π€ - proof search algorithm for boolean formulae.
- Sequent solver π€π€ - simple sequent solver.
- shari - the π£ prover.
- stupid-smt π€π€ - SMT library. Mainly project at the verification course in THU.
- Tensor Theorem Prover - first-order logic theorem prover (support unification with approximate vector similarity).
- theorem-prover - implementation of a theorem prover for first-order logic.
- Totsu π¦π¦π¦π¦π¦β - first-order conic solver for convex optimization problems .
- coq-of-rust β - formal verification for Rust.
- contracts π¦β - implements "Design By Contract" via procedural macros.
- Creusot βπ₯ - tool for deductive verification of Rust code.
- crux-mir β - static simulator for Rust programs.
- cwe_checker β - finds vulnerable patterns in binary executables.
- electrolysis βπ€ - tool for formally verifying Rust programs by transpiling them into the Lean 2 theorem prover.
- Flux πΊβπ₯Όπ₯ - refinement type checker for Rust.
- Granite βπ₯Όπ€ - find Deadlocks in Rust with Petri-Net Model checking.
- Kani π¦βπ₯Όπ₯ - bit-precise model-checker, ensures that unsafe Rust code is actually safe.
- Liquid Rust βπ€ - implement Liquid Types type checker.
- lockbud βπ₯Ό - statically detect deadlocks bugs for Rust.
- Logically Qualified Data Types - implementation of liquid types on an implicitly-typed variant of ML.
- Loom π¦β - concurrency permutation testing tool for Rust.
- matla - a manager for TLA+ projects.
- MIRAI π¦β - intended to become a widely used static analysis tool for Rust.
- MirChecker βπ₯Ό - simple static analysis tool.
- p4-analyzer - static analysis tool which checks P4 code for bugs.
- Prusti π¦π¦π¦π¦βπ₯ - prototype verifier for Rust, built upon the the Viper verification infrastructure.
- Rudra βπ₯Ό - static analyzer to detect common undefined behaviors in Rust programs.
- Rust Software Verification Benchmarks π€ - collection of Rust verification benchmarks with their verifier crates.
- Rust static analysis/verification reading and resources βΉοΈ - for further reading.
- Rust verification tools β - collection of tools/libraries about static and dynamic verification of Rust programs.
- Rust verification tools (2021) βΉοΈ - list of Rust verification tools with a bias towards βformal methodsβ tools.
- Rust verification tools list βΉοΈ - list of tools.
- RustHorn βπ₯Ό - CHC-based Automated Verification Tool for Rust.
- RustHornBelt Library & Benchmarks π₯Ό - evaluation libraries and benchmarks for the RustHornBelt PLDI paper.
- Rustproof π¦βπ€ - compiler plugin, verification condition generator.
- Shuttle π¦β - library for testing concurrent Rust code.
- Stateright π¦β - model checker for implementing distributed systems.
- VeriWasm π¦βπ₯Ό - SFI verifier of Wasm binaries.
- verus βπ₯πΊπ₯Ό - verified subset of Rust for low-level systems code.
- Xori βπ€ - static analysis library for PE32, 32+ and shellcode.
- ArcsJs - Provable - set of ArcsJs focused tools for doing proofs on ArcsJs models.
- Bounded Registers π¦β - high-assurance memory-mapped register interaction library.
- Carcara β - proof checker and elaborator for SMT proofs in the Alethe format.
- ceetle π¦π¦ - library for defining models in Computational Tree Logic and verifying their semantics.
- Chalk π¦π¦π¦π¦π¦π¦π¦β - implements the Rust trait system, based on Prolog-ish logic rules.
- Charon - interface with the rustc compiler for the purpose of program verification.
- KinΕ π - re-implementation of the core verification engine of Kind 2 model-checker.
- Kontroli π¦π¦π¦β
β¦οΈ πΊπ₯Ό - alternative implementation of the logical framework Dedukti. - Metamath-knife π¦β - verify Metamath proofs.
- Mist - userfriendly verification frontend language.
- Mizar proof checker βπ§ - Alternative Mizar proof checker.
- pocket_prover-set π¦ - base logical system for PocketProver to reason about set properties.
- rate π¦π¦π¦π¦π¦
β¦οΈ π₯Ό - clausal proof checker (DRAT, DPR) for certifying SAT solvers' unsatisfiability results. - rlfsc π¦ - checker for the LFSC proof language.
- second_opinion - verifier for Metamath Zero proof files.
- smetamath π¦βπ€ - parallel and incremental verifier for Metamath databases.
- Supervisionary π₯Ό - experimental proof-checking system for Gordon's higher-order logic.
- t3p - optimized TESC (Theory-Extensible Sequent Calculus) verifier.
- Temporal Verifier β - framework for temporal verification based on first-order linear-time temporal logic.
- verifiable-controllers β - framework to build practical, formally verified, cluster management controllers.
- Verifier π¦π€ - Trivial proof verifier - an interface to the Metamath Zero kernel.
- CNF Parser π¦π€ - efficient and customizable parser for the .cnf file format.
- DIMACS Parser π¦ - utilities to parse files in DIMACS .cnf or .sat file format.
- Exec-SAT π¦π€ - provides routines to parse SAT solver output and to execute SAT solver.
- Flussab CNF π¦ - parsing and writing of the DIMACS CNF file format.
- FRAT-rs π₯Ό - toolchain for processing and transforming files in the FRAT format.
- lalrpop-lambda π¦βπ€ - Ξ»-calculus Parser (using LALRPOP).
- Lambda Calculus Parser - Ξ»-calculus parser.
- Lambda Term Parsing - explores different parser designs for a simple lambda term grammar.
- logic-form π¦π€ - library for representing Cube, Clause, CNF and DNF.
- logic-parser π¦π - library for lexing, parsing and visualizing logical expressions.
- lp_parser_rs π¦ - LP file parser.
- mmb-parser π¦ - parser for the Metamath Zero binary proof format.
- mps π¦ - fast MPS parser.
- olean-rs π€ - parser/viewer for olean files.
- RustLogic π¦ - parsing and handling simple logical expressings.
- smt2 π¦ - SMT-LIB 2 parsing library.
- tptp π¦
β¦οΈ - parse the TPTP format.
- boolector π¦ - safe high-level bindings for the Boolector SMT solver.
- bitwuzla-sys π¦ - low-level bindings for the Bitwuzla SMT solver.
- boolector-sys π¦ - low-level bindings for the Boolector SMT solver.
- cadical-rs π¦ - bindings for the CaDiCaL SAT solver.
- cat_solver π¦ - bindings for the Kissat SAT solver.
- cplex-rs π¦π¦ - safe rust bindings for CPLEX.
- cryptominisat-rs π¦ π€ - bindings for CryptoMiniSat.
- falcon-z3 π¦ - bindings for Z3.
- highs π¦ - safe rust bindings for the HiGHS linear programming solver.
- highs-sys π¦ - bindings for the HiGHS linear programming solver.
- IPASIR π¦π€ - FFI bindings for the IPASIR incremental SAT solver interface.
- isabelle-client π¦ - client to interact with an Isabelle server.
- Kissat-rs π¦ - bindings for the Kissat SAT solver.
- lean-sys π¦ - bindings to Lean 4's C API.
- libsmt.rs π€ - bindings for SMTLIB2.
- logicng-open-wbo-sys π¦ - low-level LogicNG bindings for the MaxSAT solver Open-WBO.
- lpsolve π¦π¦π€ - high-level lpsolve wrapper.
- maxpre-rs π¦ - bindings for the (multi-objective) MaxSAT preprocessor MaxPre.
- pblib-rs π¦ - safe bindings for pblib.
- rplex π€ - bindings for CPLEX.
- rsmt2 π¦π¦β - generic library to interact with SMT-LIB 2 compliant solvers.
- russcip π¦β - safe Rust interface for SCIP.
- Rust-SMT-LIB-API π¦βπ - generic high-level API for interacting with SMT solvers.
- rust_z3prover π€ - use Z3 SMT solver from rust.
- rustproof-libsmt π¦π€ - fork of libsmt.rs.
- SAT Nexus - interfaces and wrappers for SAT solvers.
- scip-sys π¦ - raw rust bindings to SCIP.
- smt_sb-rs π¦ - Z3 SMT Simple Binding.
- smtlib π¦π¦π¦ - high-level API for interacting with SMT solvers.
- vipers - crates for interacting with the Viper verification infrastructure.
- Yices2 π¦π¦ - low and high-level bindings to the Yices2 SMT solver.
- z3 π¦π¦βπ₯ - high-level and low-level Rust bindings for the Z3 solver.
- z3-rust π¦ π€ - high level bindings for the Microsoft's Z3 SMT solver.
- Z3D π¦π€ - Z3 DSL interface.
- anthem π€ - translate answer set programs to first-order theorem prover language.
- bool2dimacs π¦ - transfer boolean expression to dimacs directly.
- CNFGEN π¦ - create boolean formulae from boolean expressions and integer expressions.
- Cnfpack π¦ - converts between DIMACS CNF file format and the compressed binary Cnfpack format.
- hz-to-mm0 π€ - translator from HOL Zero / Common HOL to Metamath Zero.
- Metamath hammer - tool for automatically proving Metamath theorems using ATPs.
- rust-smt-ir π¦π¦β - intermediate representation (IR) in Rust for SMT-LIB queries.
- AbsoluteUnity π€ - think Prolog, but less capable.
- Alice_rs π₯Όπ₯Όπ€ - implementation of a decision procedure for A Decidable Fragment of Separation Logic.
- auto π₯Ό - decision procedure for intuitionistic logic.
- Avatar Hypergraph Rewriting π¦ π€ - hypergraph rewriting system with avatars for symbolic distinction.
- coc π€ - the calculus of constructions.
- compiler π¦π€π€ - trivial compiler framework for Metamath Zero binary proofs.
- discrimination-tree π¦ - discrimination tree term indexing.
- easy-smt π¦β - easy SMT solver interaction (Inspired by the simple-smt haskell package.).
- egg π¦β - flexible, high-performance e-graph library.
- epilog π¦π€ - collection of Prolog-like tools for inference logic.
- FALL π¦π€ - easily embeddable, futures-friendly logic engine.
- foliage π¦π€ - first-order logic with integer arithmetics.
- fuzzylogic π¦ - provides operations and inference for fuzzy set theory.
- Joker Calculus π¦ - implementation of Joker Calculus in Rust.
- Kravanenn βπ€ - set of tools for Coq.
- logic-lang π¦ - structural logic based on equivalence graphs.
- logical_solver π¦ π€ - library for solving and parsing logical equations.
- LogicNG π¦ - library for creating, manipulating and solving Boolean and Pseudo-Boolean formulas.
- LogRu π¦ - small, embeddable and fast interpreter for a subset of Prolog.
- mm0-rs π¦π¦π¦βπ₯Όπ₯Ό - MM0/MM1 server and utilities.
- mmb-binutils π€ - utility tools for Metamath Zero binary proof files.
- mmb-types π¦π€ - library containing the definitions of the opcodes in the Metamath Zero binary proof files.
- moniker π¦π¦βπ€ - automagical variable binding library.
- nanoda βπ - became nanoda-lib.
- nanoda_lib - type inference/checking functionality based on the Lean theorem prover.
- nnf π¦ - Negation Normal Form manipulation library.
- polytype π¦β - Hindley-Milner polymorphic typing system.
- program-induction π¦β - library for program induction and learning representations.
- ruler
β¦οΈ βπ₯Ό - rewrite rule inference using equality saturation. - Rust First Order Logic π¦ - syntax of First Order Logic with self-consistent logical assertions.
- rust-nbe-for-mltt β - normalization by evaluation for Martin-LΓΆf Type Theory with dependent records.
- rust-smt-strings - π¦ - library for strings as defined in the SMT-LIB theory of strings.
rust-unifyπ¦ β»οΈ - unification algorithum implementation.- rustsat(2) π¦π¦π¦π¦π¦π¦ - provide elements commonly used in satisfiability solving software.
- Rusty Razor π¦π¦π¦βπ€ - tool for constructing finite models for first-order theories.
- sat_toasty_helper π¦ - convenient way to write and solve SAT constraints.
- Satoxid π¦ - library to help with encoding SAT problems.
- smt2utils π¦π¦π¦π¦π - libraries and tools for the SMT-LIB-2 standard.
- smtlib-syntax π¦ - syntactic types the for the SMT-LIB 2.6 spec. Meant for code generation, not parsing.
- term-rewriting-rs π¦ βπ€ - representing, parsing, and computing with first-order term rewriting systems.
- tribool π¦π€ - three-valued logic.
- The Trivial Metamath Zero kernel π¦π€ - Metamath Zero kernel for Trivial.
- Whisper βπ€ - logic Programming DSL.
There is numerous implementations of TAPL π, we keep only the most popular and keep an eye on implementations that worth attention.
- logic-rs πβπ€ - parser of relational predicate logic & truth tree solver
- plar-rs ππ€π» - exploring John Harrison's Handbook of Practical Logic and Automated Reasoning.
- tapl π€ - implementation of TAPL.
- TAPL in Rust βπ€ - another collection of implementations of TAPL.
- The Little Prover π - transpiled J-Bob assistant & GUI frontend.
- the-little-typer π - a Rust take on D.Friedman's book.
- tnt ππ¦ - implementation of Hofstader's "Typographical Number Theory" from the book GΓΆdel, Escher & Bach.
- types-and-programming-languages βπ€ - Exercises from Benjamin Pierce's TAPL textbook + extras!
- beta - dependently-typed programming language, aiming to support a cubical interpretation of univalence.
- egglog π¦βπ₯Ό - language that combines the benefits of equality saturation and datalog.
- Fathom π¦βπ§ - declarative data definition language for formally specifying binary data formats.
- High-order Virtual Machine (HVM) β - massively parallel, optimal functional runtime.
- isotope-prover-experiments π₯Όπ₯Όπ - experimental dependently typed language supporting borrow checking.
- Kind π¦β - next-gen functional language and proof assistant.
- Last Order Logic π¦ - experimental logical language.
- minihl - formal methods playgorund for MiniHeapLang language.
- minitt-rs π¦π¦βπ - became Voile.
- Narc π¦βπ€ - dependently-typed programming language with Agda style dependent pattern matching.
- Pika βπ§ - small, performance-oriented, dependently typed ML with algebraic effects and unboxed types..
- Pikelet π¦βπ€ - small, functional, dependently typed programming language.
- proto-vulcan π¦π¦ - miniKanren-family relational logic programming language.
- Rust pi-forall π₯Ό - partial re-implementation of pi-forall.
- Scryer Prolog π¦β - modern Prolog implementation.
- SMT-language π¦ - Sat Modulo Theory Language.
- stupid-see π€π€ - symbolic execution engine. Mainly targeted at the verification course in THU.
- Symmetric Interaction Calculus βπ - optimal Ξ»-calculus reduction. Followed devlopment now in Kind project.
- tako - experimental programming language for ergonomic software verification.
- TIP π€π€ - imperative programming language aimed at teaching fundamental concepts of static program analysis.
- Untyped Concatenative Calculus π€ - toy programming language and prototype for Dawn.
- Untyped Multistack Concatenative Calculus - toy programming language and prototype for Dawn.
- Voile π¦π¦βπ€ - became Narc.
- zz π¦βπ - zymbolic verifier and tranzpiler to bare metal C.
- Canrun π¦β - logic programming library inspired by the *Kanren family of language DSLs.
- miniKANREN π¦π€ - miniKANREN as a DSL.
- rslogic π¦βπ€ - logic programming framework for Rust inspired by Β΅Kanren.
- rust-kanren βπ€ - loose interpretation of miniKanren and cKanren.
- Β΅Kanren-rs π¦β - implementation of Β΅Kanren.
- blc π¦π€ - implementation of the binary lambda calculus.
- Closure Calculus π¦π₯Όπ€ - library for Barry Jay's Closure Calculus.
- lam - lambda calculus evaluator.
- Lamb π¦π - implementation of the pure untyped lambda calculus in modern, safe Rust.
- lambash π¦π€ - Ξ»-calculus shell.
lambda_calcπ¦β»οΈ - command-line untyped lambda calculus interpreter.- lambda_calculus π¦β - simple, zero-dependency implementation of pure lambda calculus in safe Rust.
- lambda_calculus π€ - lambda calculus with antlr grammar.
- lambdacube π§π€ - implementation of the lambda cube (and other type stuff).
- Lambdascript - educational tool illustrating beta reduction of untyped lamba terms.
- Lamcal π¦π¦π€ - lambda calculus parser and evaluator and a separate command line REPL.
- Pun Calculus π¦ - variant of Typed Lambda Calculus with generalized variable punning (ad-hoc polymorphism).
- RLCI β - Overly-documented Lambda Calculus Interpreter.
- type-theory β - typed Ξ»-calculus.
Chevreβ»οΈ - small propositional logic interpreter.- implies π¦ - storing logical formulas as parse trees and performing complex operations on them.
- logic π¦ π€π€ - crate for propositional logic.
- logic-resolver π€π€ - toy implementation of resolution for propositional logic.
- mini-prop π¦ - CLI tool for parsing and processing LaTex formatted propositional statements.
- plc π€ - propositional logic calculator.
- Plogic β - propositional logic evaluator and rule-based pattern matcher.
- Prop π¦β - library for theorem proving with Intuitionistic Propositional Logic.
- Propositional Tableaux Solver π¦ π€ - solver using the propositional tableaux method.
- prop_tune π¦π¦π¦ - library for working with Logical Propositions.
- raa_tt π¦ - prover for sentences of propositional calculus.
- Resolution Prover π€ - resolution prover library for propositional logic.
- resolution-prover π€ - Uses propositional resolution to prove statements and proofs on discord.
- rs-logik π» - propositional logic interpreter.
- rust-proplogic-toylang π€ - toy language for Propositional Logic.
- rusty-logic π€π€ - propositional logic analysis.
- simple-proof-assistant π€π€ - a proof assistant kernel for minimal propositional logic.
- validator π€ - small utility to test a propositional logic theorem prover.
- Croissant - crossword solver backed by various SAT solvers.
- formal-systems-learning-rs π€ - simulations to learn formal systems as typed first-order term rewriting systems.
- inf402 - SAT-solver-based takuzu solver.
- Junglefowl π¦π¦ - runs Peano arithmetic on Rust types, verified at compile time..
- list-routine-learning-rs π€ - to learn typed first-order term rewriting systems that perform list routines.
- logical_tui π€ - tui for logical_solver.
- Minimal models π€ - uses a SAT solver to find minimal partial assignments that are model of a CNF formula.
- n-queens-sat π€ - modelling n-queens problem as conjunctive normal form and solving it with DPLL algorithm.
- nonogrid π¦ - lightning fast nonogram solver.
- peano π₯Ό - An environment for learning formal mathematical reasoning from scratch.
- Relog - implementation of several strongly-normalizing string rewriting systems.
- rummy_to_sat - implementation of a solver for Rummy.
- rust-z3-practice π€ - solving a number of SAT problems using Z3.
- sudoku_sat - solve Sudoku variants with SAT solvers.
- Supermux π€ - reduction of the superpermutation problem to Quantified Boolean Formula.
- Supersat π€ - attempt to find superpermutations by reducing the problem to SAT.
- tarpit-rs βπ€ - type-level implementation of Smallfuck. Turing-completeness proof for Rust's type system.
- VeriFactory β - verifier for Factorio blueprints.
- Verification for Dummies: SMT and Induction - broadly discusses induction as a formal verification technique.
- Verification of a Rust Implementation of Knuth's Dancing Links using ACL2 - 2023.
- Specifying and Verifying Higher-order Rust Iterators - 2023.
- RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code - 2022.
- Hardware/Software Co-Assurance using the Rust Programming Language and ACL2 - 2022.
- Extensible Functional-Correctness Verification of Rust Programs by the Technique of Prophecy - 2021.
- Understanding and Evolving the Rust Programming Language - 2020.
- Simple Verification of Rust Programs via Functional Purification - 2016.
- Artifact Evaluation: Kani Rust Verifier π₯Ό - Kani Rust Model Checker artifact for ICSE 2022 Artifact Evaluation.
- flux-demo - small examples that demonstrate how flux works.
- rust-smt-ir-examples - examples of using a rust-smt-ir, a Rust intermediate representation (IR) for SMT-LIB.
- aws-lambda-z3 - tutorial on running Z3 on AWS Lambda, with Rust.
- A Formal Verification of Rust's Binary Search Implementation. π¬π§
- Formal Land π¬π§
- Kani Rust Verifier Blog π¬π§
- Mist Blog π¬π§
- Splr notebook. π―π΅
- Research notebook about improving with Rust the performance of nonclausal automated theorem provers. π¬π§
β¦οΈ - Articles about a collection of tools/libraries to support both static and dynamic verification of Rust programs. π¬π§
- Varisat notebook. π¬π§
β¦οΈ
- Cracking the Cryptic (with Z3 and Rust) - 2024
- How Open Source Projects are Using Kani to Write Better Software in Rust - 2023.
- Check AI-Generated Code Perfectly and Automatically - 2023.
- Solving The Witness with Z3 - 2022.
- Formally Verifying Rust's Opaque Types - 2022.
- An adventure with optimization, Rust and Z3 - 2019.
- solver - 116 entries. π―
- logic - 83 entries. π―
- smt - 41 entries. π―
- verification - 38 entries. π―
- sat - 37 entries. π―
- satisfiability - 26 entries. π―
- linear-programming - 15 entries. π―
- proving - 13 entries. π―
- smt-lib - 12 entries. π―
- cnf - 10 entries. π―
- rewriting - 9 entries. π―
- prover - 8 entries. π―
- first-order - 6 entries. π―
- z3 - 6 entries. π―
- dependent-types - 6 entries. π―
- metamath-zero - 5 entries. π―
- dimacs - 5 entries. π―
- Mikko Aarnos - Serkr.
- Johannes Altmanninger - rate.
- ammkrn - nanoda, nanoda_lib, second_opinion.
- Bruno Andreotti - Carcara.
- Arata - lutrix.
- arbaregni - resolution-prover.
- astrobeastie - sequentprover.
- Yechan Bae - Rudra, Satire.
- Clark Barrett - Rust-SMT-LIB-API.
- Mathieu Baudet - smt2utils.
- Mike Beaumont - rust-sat.
- Antoine Belvire - Croissant.
- Tim Beurskens - RsBDD.
- Matteo Biggio - cplex-rs.
- Justin Blanchard - cat_solver.
- boitsov14 - theorem-prover-rs.
- James Bornholt - rustsat, Shuttle.
- Henrik BΓΆving - Obvious.
- Oliver BΓΈving - Mist, smtlib, vipers.
- Lee ByeongJun - Lambda Calculus Parser.
- Bickio O'Callahan - Solving The Witness with Z3.
- Mario Carneiro - FRAT-rs, hz-to-mm0, Metamath hammer, Metamath-knife, Mizar proof checker, mm0-rs, olean-rs.
- Tej Chajed - Temporal Verifier.
- Adrien Champion - hoice, KinΕ, matla, Mikino, rsmt2, SAT-MICRO, Verification for Dummies.
- David Chanin - Tensor Theorem Prover.
- Michelle Cheatham - rusty-logic.
- Jimmy Chen Chen - theorem-prover.
- Alex Chew - Z3D.
- Konstantin Chukharev - SAT Nexus.
- Guillaume Claret - coq-of-rust, Formal Land.
- Cobalt - SAT solver ANalyser.
- Lorenzo Colombini - Colombini-SAT.
- convexbrain - Totsu.
- David Cox - mps.
- Simon Cruanes - BatSat.
- Dacit - Sequent solver.
- dandxy89 - lp_parser_rs.
- Azeez Daoud - ceetle.
- DavidD12 - SMT-language, smt_sb-rs.
- Ariel Davis - coc.
- Xavier Denis - Creusot, RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code, RustHornBelt Library & Benchmarks, Rust verification tools (2021), Specifying and Verifying Higher-order Rust Iterators.
- Sushant Dinesh - libsmt.rs.
- Sylvie Dirkswager - Pika.
- Craig Disselkoen - boolector.
- Mark Drobnak - p4-analyzer.
- Bruno Dutertre - rust-smt-ir, rust-smt-ir-examples, rust-smt-strings.
- Thomas Dziedzic - lambda_calculus.
- Kurt Ehlert - ellp.
- Trevor Elliott - auto, easy-smt.
- endeav0r - falcon-z3.
- Enkelmann - cwe_checker.
- Aodhnait ΓtaΓn - Esther.
- Michael FΓ€rber - CoP, Kontroli, Lambda Term Parsing, meancop, research notebook about improving with Rust the performance of nonclausal automated theorem provers.
- Nathan Fenner - sat_toasty_helper.
- FireFighterDuck - Alice_rs, Kissat-rs, minihl.
- Paolo Flores - logic-parser.
- Hugo Frezat - logic-lang.
- Robin Freyler - CNF Parser, DIMACS Parser, Stevia.
- Galois, Inc. - crux-mir.
- Alexey Gerasimov - Liquid Rust.
- Jad Ghalayini - isotope-prover-experiments, lean-sys.
- Mohammed Ghannam - russcip, scip-sys.
- Nathan Graule - rs-logik.
- Brandon H. Gomes - qbar.
- Robert Grosse - cryptominisat-rs.
- Masaki Hara - Logic solver, RatSat.
- Jannis Harder - Cnfpack, Flussab CNF, Minimal models, starlit, Varisat, Varisat notebook.
- David S. Hardin - Hardware/Software Co-Assurance using the Rust Programming Language and ACL2, Verification of a Rust Implementation of Knuth's Dancing Links using ACL2.
- Rowan Hart - Yices2.
- TimothΓ©e Haudebourg - smt2.
- Reuben Hillyard - beta.
- Son HO - Charon.
- Sarek HΓΈverstad SkotΓ₯m - CreuSAT.
- Hoblovski - stupid-see, stupid-smt.
- Emil Hofstetter - mini-prop, prop_tune.
- hrkzmnm - rust_z3prover.
- Tero Huttunen - proto-vulcan.
- Christoph Jabs - Scuttle, maxpre-rs, rustsat(2).
- Jan - Plogic.
- Ranjit Jhala - flux-demo.
- Andrew Johnson - LSTS, Pun Calculus, Relog.
- Evan Johnson - VeriWasm.
- Dylan R. Johnston - Formally Verifying Rust's Opaque Types.
- Matthias Jugan - LogicNG, logicng-open-wbo-sys.
- Ralf Jung - Understanding and Evolving the Rust Programming Language.
- Carl Kadie - Check AI-Generated Code Perfectly and Automatically.
- Hosein Kalbasi - akim.
- Igor Kalichevski - nnf.
- karroffel - contracts.
- Anto KeinΓ€nen - logical_solver, logical_tui.
- Rahul Kumar - How Open Source Projects are Using Kani to Write Better Software in Rust.
- Prateek Kumar - msat, rsat, slp, SolHOP.
- Alexey Kutepov - Noq.
- Ivan Ladelshchikov - nonogrid.
- Andrea Lattuada - verus.
- lcnr - cobalt.
- Shea Leffler - tarpit-rs, whisper.
- Alessandro Legnani - VeriFactory.
- Nico Lehmann - Flux.
- Carl Lerche - Loom.
- Chuck Liang - Lambdascript.
- Nathan Lilienthal - lambash, lalrpop-lambda.
- ljedrz - blc, lambda_calculus.
- Ophir LOJKINE - highs, highs-sys, good_lp.
- Emmanuel Lonca - pblib-rs.
- Kevin Lotz - isabelle-client.
- Patrick LΓΌhne - anthem, foliage.
- Michael Madden - Xori.
- Scott J Maddox - Untyped Concatenative Calculus, Untyped Multistack Concatenative Calculus.
- Indraneel Mahendrakumar - Lamb.
- Harald Maida - Lamcal.
- Krzysztof MaΕysa - prover.
- Manas - fuzzylogic.
- Miklos Maroti - cadical-rs, relsat-rs, uasat-rs.
- marshtompsxd - verifiable-controllers.
- Niko Matsakis - Chalk, Kani, plar-rs.
- Yusuke Matsushita - Extensible Functional-Correctness Verification of Rust Programs by the Technique of Prophecy, RustHorn.
- mbillingr - miniKANREN, The Little Prover, the-little-typer.
- mcmfb - lambda_calc.
- Tom Meyer - Granite.
- Alexander Mishunin - minisat-rust.
- Proloy Mishra - lam, nnoq, nyaya.
- Bruce Mitchener - z3.
- Lucas Morales - polytype, program-induction.
- Jesse Mu - satyrs.
- Dominic Mulligan - Supervisionary.
- Jon Nadal - Stateright.
- Chandrakana Nandi - Ruler.
- neuring - rummy_to_sat, Satoxid.
- Sven Nilsen - Avalog, Avatar Hypergraph Rewriting, Caso, Debug-SAT, Joker Calculus, Last Order Logic, linear_solver, Monotonic-Solver, pocket_prover, pocket_prover-set, Poi, Prop, reachability_solver.
- Yuichi Nishiwaki - shari.
- Stefan O'Rear - smetamath.
- Robert Obkircher - sat-solver.
- Adolfo OchagavΓa - An adventure with optimization, Rust and Z3.
- Edgar Onghena - inf402.
- Alex Ozdemir - rlfsc.
- Chris Patuzzo - Supermux, Supersat.
- Pierre-Marie PΓ©drot - Kravanenn.
- Hugo Peters - Cracking the Cryptic (with Z3 and Rust).
- Arvid E. Picciani - zz.
- Dan Pittman - Bounded Registers.
- Gabriel Poesia - peano.
- Nadia Polikarpova - cyclegg.
- Christian Poveda - Chevre.
- Bobby Powers - Logically Qualified Data Types.
- Joshua Pratt - ArcsJs - Provable, tako.
- petersn - autosat.
- Boqin Qin - lockbud.
- Armaan Rashid - implies.
- Michael Rawson - discrimination-tree, lazyCoP, lerna, lickety, SATCoP, tptp.
- Alastair Reid - Articles about a collection of tools/libraries to support both static and dynamic verification of Rust programs, Rust Software Verification Benchmarks, Rust verification tools, Rust verification tools list.
- Adrien Renaudineau - sat_lab.
- Corey Richardson - lpsolve.
- Nathan Ringo - FALL.
- Benjamin Rogers-Newsome - Rust First Order Logic.
- Erik Rohkohl - n-queens-sat.
- Marco Concetto Rudilosso - validator.
- Josh Rule - formal-systems-learning-rs, list-routine-learning-rs, term-rewriting-rs.
- Salman Saghafi - rust-z3-practice, Rusty Razor.
- Michael Salter - Rustproof, rustproof-libsmt.
- Daniel Schemmel - DRSAT.
- Ryan Schroeder - AbsoluteUnity, epilog.
- Carol Schulze - gpp-solver.
- Klas Segeljakt - type-theory.
- shinkwhek - SAT solver.
- skbaek - t3p.
- Narazaki Shuji - SAT-bench, Splr, Splr notebook, sudoku_sat.
- JΓΆrg Singer - raa_tt.
- J David Smith - rplex.
- SnOβWMaN - rust-proplogic-toylang.
- snsinfu - dpll-sat.
- Mikhail Solovev - bitwuzla-sys, boolector-sys.
- Dennis Sprokholt - aws-lambda-z3, Rust pi-forall.
- Will Sturgeon - Junglefowl.
- Yuheng Su - logic-form.
- SymmetricChaos - tnt.
- Mateusz Szpakowski - CNFGEN, Exec-SAT.
- Lucas Tabary-Maujean - Proost.
- Victor Taelin - High-order Virtual Machine (HVM), Kind2, Symmetric Interaction Calculus..
- Calin Tataru - homotopy-rs.
- Mark Thom - Scryer Prolog.
- Fabian Thorand - LogRu.
- Hitoshi Togasaki - scrapsat, screwsat.
- Callum Tolley - plc
- Aaron Trent - tribool.
- Sebastian Ullrich - A Formal Verification of Rust's Binary Search Implementation, electrolysis, Simple Verification of Rust Programs via Functional Purification.
- V4kst1z - tapl, TIP.
- Alexa VanHattum - Artifact Evaluation: Kani Rust Verifier (Kani).
- Pavol VargovΔΓk - z3-rust.
- Herman Venter - MIRAI, Rust static analysis/verification reading and resources.
- Mark Verleg - prover(2).
- Nikita Voronov - RLCI.
- Shuxian Wang - QED Prover.
- Max Willsey - egg, egglog.
- Ivo Wingelaar - compiler, mmb-binutils, mmb-parser, mmb-types, The Trivial Metamath Zero kernel, Verifier.
- Jan Winkelmann - smtlib-syntax.
- Jieyou Xu - Propositional Tableaux Solver.
- Ren Yanjie - bool2dimacs, RustLogic.
- Brendan Zabarauskas - Fathom, moniker, Pikelet, rust-nbe-for-mltt.
- Bas Zalmstra - Resolvo.
- Alexey Zatelepin - minilp.
- Eric Zhang - Β΅Kanren-rs.
- Hanliang Zhang - sat.
- Tesla Ice Zhang - minitt-rs, Narc, Voile.
- Felix Zhu - lambdacube.
- Li Zhuohua - MirChecker.