About

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.

Contents

• Projects
  • Provers & Solvers
    • Provers TPTP compliant
    • SAT Solver
    • Solver MPS compliant
    • Proof assistant
    • Misc
  • Verification
    • Static Analysis & Rust verification tools
    • Misc
  • Libraries
    • Parser
    • Bindings
    • Translator
    • Misc
  • Books code
  • Programming Language
  • Kanren
  • Lambda Calculus
  • Propositional Logic
  • Unclassified
• Resources
  • Books
  • Crates keywords
  • Research Paper & Thesis
  • Demos
  • Blogs
  • Posts
  • Community

---

Legend

• 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 🚧

Projects

Provers and Solvers

Provers TPTP compliant

• 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.

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.
• 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.

Solver MPS compliant

• ellp 📦🚧 - linear programming library that provides primal and dual simplex solvers.
• minilp 📦⭐💀 - linear programming solver.

Proof assistant

• 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.

Misc

• 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 .

Verification

Static Analysis & Rust verification tools

• 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.

Misc

• 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.

Libraries

Parser

• 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.

Bindings

• 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.

Translator

• 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.

Misc

• 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.

Books code

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!

Programming Language

• 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.

Kanren

• 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.

Lambda Calculus

• 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.

Propositional logic

• 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.

Unclassified

• 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.

Resources

Books

• Verification for Dummies: SMT and Induction - broadly discusses induction as a formal verification technique.

Research Paper & Thesis

• 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.

Demos

• 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.

Blogs

• 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. 🇬🇧♦️

Posts

• 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.

Crates keywords

• 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. 💯

Community

• 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.