Skip to content

An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.

License

Notifications You must be signed in to change notification settings

newca12/awesome-rust-formalized-reasoning

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 

Repository files navigation

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


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 ℹ️
  • Paper with code 🏭
  • Popular ⭐
  • Research paper 🥼
  • 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.
  • 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.

SAT Solver

  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • microlp 📦 - linear programming solver (fork of minilp).
  • 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.
  • minimo 🥼🥼♦️⭐ - An environment for learning formal mathematical reasoning from scratch.
  • 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.
  • 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.
  • 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/framework

Misc

Libraries

Parser

Bindings

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.
  • 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.
  • rust-smt-ir 📦📦⭐ - intermediate representation (IR) in Rust for SMT-LIB queries.

Misc

Books code

There is numerous implementations of TAPL 📖, we keep only the most popular and keep an eye on implementations that worth attention.

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

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 Logic 📦🎓 - propositional Logic Library .
  • 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.
  • 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.
  • 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

Research Paper & Thesis

Demos

Blogs

Posts

Crates keywords

Community

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.

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published