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 ℹ️
- Paper with code 🏭
- Popular ⭐
- Research paper 🥼
- Toy project 🐤
- Video 📺
- Web demo 👀
- WIP 🚧
- CoP 📦 - reimplement automated theorem provers of the leanCoP family, such as leanCoP and nanoCoP.
- HopCoP - theorem prover for first-order logic based on connection tableaux and backjumping.
- lazyCoP ⌚💤 - automatic theorem prover for first-order logic with equality.
- lerna 💀 - proves theorems.
- lickety 💤 - prototype system for linear resolution with splitting.
- meancop 📦♻️ - became CoP.
- res-rs 🚧 - first bits for first-order logic prover.
- Serkr ⭐👻 - automated theorem prover for first order logic with equality.
- theorem-prover-rs - rewrite of theorem-prover-kt a sequent-style automated theorem prover.
- backdoor-solver - backdoor-based SAT solver.
- 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.
- logiq 📦 - a Domain-Specific Language for SAT Solving and a solver using advanced SAT solving algorithms.
- lutrix 💤 - SAT/SMT Solver.
- m2cSMT 📦 - solver of non-linear (in)equations encoded in a subset of the SMT-Lib format.
- microsat 📦 - tiny DPLL SAT-solver.
- minisat-rust ⭐💤 - experimental minisat SAT solver.
- msat 📦💀 - MaxSAT Solver.
- NanoSAT 🚧 - almost-efficient implementation of the Conflit-Driven Clause Learning (CDCL) framework.
- otter_sat 📦 - CDCL SAT solver written for skill and research.
- 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(2) 🐤💤 - toy SAT solver.
- sat - simple CDCL sat solver.
- satsol 🐤 - some SAT solving algorithms for DIMACS inputs.
- SAT solver 🐤💤 - SAT solver.
- SAT Solver(2) 🐤 - simple 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.
- SAT-Solver - DPLL and CDCL Solver.
- 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.
- simple-sat - one of the SAT solvers of all time.
slp📦♻️ - became SolHOP.- SolHOP 📦💀 - aims to be a SAT and MaxSAT solver. Currently, a CDCL based SAT.
- Splr 📦
♦️ ⭐ - modern CDCL SAT solver. - StalmarckSAT 📦 - SAT solver based on the Stålmarck Procedure.
- 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.
- microlp 📦 - linear programming solver (fork of minilp).
- minilp 📦⭐💀 - linear programming solver.
- Acorn ⭐ - theorem prover with built-in AI assistant.
- Canonical 🥼📺📺
♦️ ⭐ - solver for type inhabitation in dependent type theory. cobalt♻️👻 - a wip minimal proof assistant.- Croof ⭐ - simple math proof tool for simple math expressions.
- Esther 💤 - simple automated proof assistant.
- hakim - hacky interactive theorem prover.
- homotopy-rs 🥼🥼
♦️ ⭐ - implementation of homotopy.io proof assistant. - LSTS 📦⭐ - proof assistant that is also a programming language.
- minimo 🥼🥼
♦️ ⭐ - An environment for learning formal mathematical reasoning from scratch. - nnoq - simple theorem prover (nay, verifier) based on functional expression rewriting.
- Noq 📺⭐ - Not Coq. Simple expression transformer that is not Coq.
- nyaya - proof language based on sequent calculus and Metamath.
- Poi 📦⭐ - pragmatic point-free theorem prover assistant.
- Proost - simple proof assistant.
- qbar 📦💤 - experimental automated theorem verifier/prover and proof assistant.
- shari - proof assistant based on the internal language of topos with NNO (intuitionistic higher-order arithmetic).
- Avalog 📦⭐ - experimental implementation of Avatar Logic with a Prolog-like syntax.
- autosat 📦🐤 - automatic conversion of functions to CNF for SAT solving.
- Axiom Profiler 2.0 🥼⭐ - profiler for exploring and visualizing SMT solver quantifier instantiations.
- bootfrost - automated theorem proving program for first-order formulas with extensions.
- 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.
- INCL Automated Theorem Prover 📖👀 - multi logic theorem prover based on Graham Priests 2008 book.
- 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.
- 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.
- Rustplex 📦 - a linear programming solver based on the Simplex algorithm.
- 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.
- SMTSCOPE - 📦⭐ - automatically analyses and visualises SMT solver execution traces.
- 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 .
- Charon ⭐🥼🔥 - interface with the rustc compiler for the purpose of program verification.
- 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.
- Hax 📦⭐🥼 - tool for high assurance translations of a large subset of Rust into formal languages (F*, Rocq, ...).
- 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.
- Machine-check 📦📦📦📦📦📦📦📦📦📦📦 - formal verification tool for digital systems.
- 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.
- r2u2_core 📦🥼 - Realizable, Reconfigurable, Unobtrusive Unit (R2U2) stream-based runtime verification.
- RefinedRust 🥼 - type system for high-assurance verification of Rust Programs.
- rIC3 Hardware Model Checker 📦⌚⭐ - high-performance implementation of the IC3/PDR algorithm.
- 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 std-lib verification 📺⭐ - verifying the Rust standard library.
- 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.
- VeriFast ⭐ - research prototype tool for modular formal verification of C, Rust and Java programs.
- VeriWasm 📦⭐🥼 - SFI verifier of Wasm binaries.
- verus ⭐🔥📺🥼 - verified subset of Rust for low-level systems code.
- vostd - formal verification of Asterinas OSTD with Verus.
- 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.
- 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.
- rust-metamath 💤 - Metamath verifier.
- 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.
- coq-rs - this program can parse Coq .vo files.
- 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.
- isabelle export tool - parser for isabelle database files.
- 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.
- Patronus 📦🚧 - btor2 parser, wip hardware bug-finding toolkit.
- 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.
- cadical-sys 📦 - almost complete safe and unsafe bindings for the CaDiCal SAT solver.
- cat_solver 📦 - bindings for the Kissat SAT solver.
- clingo-rs 📦📦📦⭐ - idiomatic bindings to the clingo library.
- cplex-rs 📦📦 - safe rust bindings for CPLEX.
- cryptominisat-rs 📦💤 - bindings for CryptoMiniSat.
- EasyZ3 📦 - simplified API to get started with the z3 SAT solver.
- 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.
- Ipasir-loading 📦 - load shared libraries of IPASIR compatible SAT solvers.
- 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.
- rsmaxsat 📦 - bindings for EvalMaxSAT .
- rsmt2 📦📦⭐💤 - generic library to interact with SMT-LIB 2 compliant solvers.
- rssat 📦💀 - bindings for multiple popular SAT solvers, superseded by satgalaxy-rs.
- 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.
- satgalaxy-rs 📦 - FFI bindings for satgalaxy-core bringing high-performance SAT solving to Rust.
- 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.
- Decdnnf-rs 📦 - translating formulas generated by d4 into the format generated by c2d.
- hz-to-mm0 💤 - translator from HOL Zero / Common HOL to Metamath Zero.
- Metamath hammer - tool for automatically proving Metamath theorems using ATPs.
- pindakaas 📦📦📦📦📦📦 - transform integer and pseudo Boolean constraints into conjunctive normal form.
- 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 📦📦📦📦📦📦📦📦📦⭐ - 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.
- program-proofs-prusti 📖 - examples and exercises from the book Program Proofs by K. Rustan M. Leino.
- tapl 💤 - implementation of TAPL.
- TAPL Implementations - collection of implementations of TAPL (Chap 3-7,9,11,13-14,19,22).
- TAPL in Rust ⭐💤 - collection of implementations of TAPL (Chap 3-10,17,25).
- 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 TAPL textbook + extras! (Chap 5-7,9-10)
- 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.
- Interaction Calculus 📦⭐ - programming language (fit the optimal λ-calculus reduction algorithm perfectly).
- 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.
- norem-lang - pure functional programming language with automatic verification and effect system.
- 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.
- reckon ⭐ - programming language designed for reasoning tasks, proof checking, and logical inferencing.
- rooc 🎓⭐ - a language for compiling formal mathematical models into static models.
- 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.
- tako - experimental programming language for ergonomic software verification.
- TIP 🐤💤 - 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).
- Lambda Shell 📦 - simple REPL shell for untyped lambda expressions.
- Lambdascript - educational tool illustrating beta reduction of untyped lamba terms.
- Lamcal 📦📦💤 - lambda calculus parser and evaluator and a separate command line REPL.
- lalrpop-lambda 📦⭐ - λ-calculus grammar/interpretor written using LALRPOP and
λ!. - 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.
- Logic Tracer 📦 - reads a logical proposition and interprets it to build the truth table and the AST.
- 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 Logic 📦🎓 - propositional Logic Library.
- Propositional logic evaluator 📦 - propositional logic evaluator (truth tables for propositional expressions).
- 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.
- type-proof 📦📦 - crate for type-checked propositional logic proofs.
- 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.
- Hashi - Bridges Puzzle - Hashi Puzzle (aka Bridges) solver.
- 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.
- Relog - implementation of several strongly-normalizing string rewriting systems.
- roq 📦📦 - proc-macro Coq code generation and proof automation.
- rummy_to_sat - implementation of a solver for Rummy.
- rust-z3-practice 💤 - solving a number of SAT problems using Z3.
- Satisfaction 🥼 - investigate phase transitions in k-SAT problems.
- 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.
- Type System Chess ⭐ - chess implemented entirely in the Rust type system.
- VeriFactory ⭐ - verifier for Factorio blueprints.
- Verification for Dummies: SMT and Induction - broadly discusses induction as a formal verification technique.
- How to discover short, shorter, and the shortest proofs of unsatisfiability🏭 - 2024
- A hybrid approach to semi-automated Rust verification - 2024.
- 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. 🇬🇧
♦️
- Visions of the future: formal verification in Rust - 2024
- Some notes on Rust, mutable aliasing and formal verification
♦️ - 2024 - 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 - 155 entries. 💯
- logic - 134 entries. 💯
- verification - 101 entries. 💯
- sat - 51 entries. 💯
- smt - 47 entries. 💯
- satisfiability - 37 entries. 💯
- linear-programming - 21 entries. 💯
- proving - 16 entries. 💯
- smt-lib - 12 entries. 💯
- prover - 12 entries. :100
- cnf - 10 entries. 💯:
- sat-solver - 10 entries. 💯
- rewriting - 9 entries. 💯
- z3 - 9 entries. 💯
- first-order - 6 entries. 💯
- dependent-types - 6 entries. 💯
- dimacs - 6 entries. 💯
- metamath-zero - 5 entries. 💯
- Mikko Aarnos - Serkr.
- Johannes Altmanninger - rate.
- ammkrn -
nanoda, nanoda_lib, second_opinion. - Bruno Andreotti - Carcara.
- Arata - lutrix.
- arbaregni - resolution-prover.
- astrobeastie - sequentprover.
- Alexis Aurandt - r2u2_core.
- 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.
- Aurel Bílý - program-proofs-prusti.
- Justin Blanchard - cat_solver.
- boitsov14 - theorem-prover-rs.
- James Bornholt - rustsat(2), Shuttle.
- Henrik Böving - Obvious.
- Oliver Bøving - Mist, smtlib, vipers.
- Lee ByeongJun - Lambda Calculus Parser.
- Bickio O'Callahan - Solving The Witness with Z3.
- Pierre Carbonnelle - m2cSMT.
- Mario Carneiro - coq-rs, FRAT-rs, hz-to-mm0, isabelle export tool, 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.
- Thomas Chaumeny - Satisfaction.
- Jimmy Chen Chen - theorem-prover.
- Alex Chew - Z3D.
- Konstantin Chukharev - SAT Nexus, backdoor-solver.
- Guillaume Claret - coq-of-rust, Formal Land.
- Cobalt - SAT solver ANalyser.
- CoCoSol - logiq.
- 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.
- Liam Davis - StalmarckSAT.
- Jip J. Dekker - pindakaas.
- 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 (2023), A hybrid approach to semi-automated Rust verification (2024), Visions of the future: formal verification in Rust.
- Sushant Dinesh - libsmt.rs.
- Sylvie Dirkswager - Pika.
- Craig Disselkoen - boolector.
- Andrei Dobrescu - INCL Automated Theorem Prover.
- Dragon-Hatcher - Type System Chess.
- 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.
- Jonáš Fiala - SMTSCOPE.
- FireFighterDuck - Alice_rs, Kissat-rs, minihl.
- Paolo Flores - logic-parser.
- Hugo Frezat - logic-lang.
- Robin Freyler - CNF Parser, DIMACS Parser, Stevia.
- Lennard Gäher - RefinedRust.
- 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.
- Vinicius Gomes - NanoSAT, satsol.
- William Goodall - roq.
- Robert Grosse - cryptominisat-rs.
- Alexandru Jercan - Croof.
- 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.
- Graydon Hoare - Some notes on Rust, mutable aliasing and formal verification.
- Emil Hofstetter - mini-prop, prop_tune.
- Khaled Hosseini - Propositional logic evaluator.
- hrkzmnm - rust_z3prover.
- Tero Huttunen - proto-vulcan.
- Noel Huibers - Hashi - Bridges Puzzle.
- Christoph Jabs - Scuttle, maxpre-rs, rustsat.
- Bart Jacobs - VeriFast.
- Jan - Plogic.
- Paweł Jastrzebski - Propositional Logic.
- 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.
- Oskari Jyrkinen - Axiom Profiler 2.0.
- jzbor - Lambda Shell.
- Carl Kadie - Check AI-Generated Code Perfectly and Automatically.
- Hosein Kalbasi - akim.
- Igor Kalichevski - nnf.
- karroffel - contracts.
- Anto Keinänen - logical_solver, logical_tui.
- Franziskus Kiefer - Hax.
- Rahul Kumar - How Open Source Projects are Using Kani to Write Better Software in Rust, Rust std-lib verification.
- Prateek Kumar -
msat,rsat,slp,SolHOP. - Alexey Kutepov - Noq.
- Kevin Lacker - Acorn.
- Ivan Ladelshchikov - nonogrid.
- Kevin Laeufer - Patronus.
- Aleksandr Larionov - bootfrost.
- 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 - Decdnnf-rs, Ipasir-loading, pblib-rs.
- Kevin Lotz - isabelle-client.
- Andrew Luka - cadical-sys.
- 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.
- MarcoTz - TAPL Implementations.
- 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.
- adam mcdaniel - reckon.
- 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.
- Chase Norman - Canonical.
- Stefan O'Rear - smetamath.
- Robert Obkircher - sat-solver.
- Adolfo Ochagavía - An adventure with optimization, Rust and Z3.
- Jan Onderka - Machine-check.
- Edgar Onghena - inf402.
- Alex Ozdemir - rlfsc.
- Mohsen Pakzad - Rustplex.
- PatrickTheElder - EasyZ3.
- Chris Patuzzo - Supermux, Supersat.
- Pierre-Marie Pédrot - Kravanenn.
- Hugo Peters - Cracking the Cryptic (with Z3 and Rust).
- Arvid E. Picciani - zz.
- Anton Ping - norem-lang.
- Dan Pittman - Bounded Registers.
- Gabriel Poesia - minimo.
- 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, HopCoP, 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.
- Fernando Bryan Reza Campos - Logic Tracer.
- 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.
- Robert Scheidegger - microsat.
- 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.
- Konstantin Sidorov - How to discover short, shorter, and the shortest proofs of unsatisfiability, simple-stat.
- Jörg Singer - raa_tt.
- J David Smith - rplex.
- SnO₂WMaN - rust-proplogic-toylang.
- snsinfu - dpll-sat.
- Mikhail Solovev - bitwuzla-sys, boolector-sys.
- Ben Sparkes - otter_sat.
- Specy - microlp, rooc.
- Dennis Sprokholt - aws-lambda-z3, Rust pi-forall.
- Will Sturgeon - Junglefowl.
- Yuheng Su - logic-form, rIC3 Hardware Model Checker.
- SymmetricChaos - tnt.
- Mateusz Szpakowski - CNFGEN, Exec-SAT.
- Lucas Tabary-Maujean - Proost.
- Victor Taelin - High-order Virtual Machine (HVM), Kind2, Interaction Calculus.
- Calin Tataru - homotopy-rs.
- Sven Thiele - clingo-rs.
- Mark Thom - Scryer Prolog.
- Fabian Thorand - LogRu.
- Hitoshi Togasaki - scrapsat, screwsat.
- Callum Tolley - plc.
- William Towler - type-proof.
- 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).
- Nathaniel Victor - SAT Solver(2).
- Nikita Voronov - RLCI.
- Xinyi Wan - vostd.
- John Wang - rust-metamath.
- 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.
- Florian Würmseer - SAT-Solver.
- 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. - Xie Zhongtao - rsmaxsat,
rssat, satgalaxy-rs. - Felix Zhu - lambdacube.
- Li Zhuohua - MirChecker.
- Philip Zucker - res-rs.