• Stars
    star
    289
  • Rank 143,419 (Top 3 %)
  • Language
  • License
    MIT License
  • Created over 3 years ago
  • Updated 3 months ago

Reviews

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Repository Details

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

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

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.
  • 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 Rust SAT solver.
  • sat - simple CDCL sat solver.
  • SATCoP - theorem prover for first-order logic based on connection tableau and SAT solving.
  • Satire 📦 - educational SAT solver.
  • satyrs 🎓💤 - DPLL SAT solver.
  • SAT-MICRO 🥼 - reimplementation of the SAT-solver described in 'SAT-MICRO: petit mais costaud!'.
  • SAT solver 🐤💤 - 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.

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.
  • Caso 📦 - category Theory Solver for Commutative Diagrams.
  • Cosette Prover🥼 - reimplementation of the Cosette prover in Rust.
  • cyclegg - cyclic theorem prover for equational reasoning using egraph.
  • 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.
  • minilp 📦⭐💀 - linear programming solver.
  • 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.
  • 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.
  • 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-rs 🚧 - rewrite of theorem-prover-kt a sequent-style automated theorem prover.
  • Totsu 📦📦📦📦📦⭐ - first-order conic solver for convex optimization problems .

Verification

Static Analysis & Rust verification tools

Misc

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 Term Parsing - explores different parser designs for a simple lambda term grammar.
  • logic-form 📦🐤 - library for representing Cube, Clause, CNF and DNF.
  • mmb-parser 📦 - parser for the Metamath Zero binary proof format.
  • 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

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

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

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.
  • RLCI ⭐ - Overly-documented Lambda Calculus Interpreter.

Propositional logic

  • Chevre ♻️ - small propositional logic interpreter.
  • 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.
  • 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

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

Resources

Books

Research Paper & Thesis

Demos

Blogs

Posts

Crates keywords

Community

More Repositories

1

scala-netty-examples

Scala port of the examples from Jboss Netty distribution
Scala
72
star
2

dictionary-builder

Real world example to demonstrate advanced techniques to unmarshall very large xml document with very low memory footprint.
Rust
58
star
3

scala-atp

Examples from John Harrison's "Handbook of Practical Logic and Automated Reasoning", ported to Scala
Scala
13
star
4

ocaml-atp

Code from John Harrison's Handbook of Practical Logic and Automated Reasoning
OCaml
8
star
5

haskell-atp

Examples from John Harrison's "Handbook of Practical Logic and Automated Reasoning", ported to Haskell
Haskell
8
star
6

parse_mediawiki_dump

parse_mediawiki_dump clone
Rust
5
star
7

TMDb-async-client

Scala async wrapper for TMDb (The Movie Database) API
Scala
3
star
8

TMDb-shelf

JavaFX client for TMDb (The Movie Database)
Scala
2
star
9

shakuntala-devi-trainer

Brain training tool inspired by Shakuntala Devi's technics
Rust
1
star
10

gourmand-web-viewer

Web viewer for Gourmand Recipe Manager
Rust
1
star
11

VersatiList

A multi-platform dynamic list filter
Rust
1
star
12

multi-machine-dedup

Deduplication tool using SQLite to allow multi-machine features.
Rust
1
star
13

playground-rs

Rust playground
Rust
1
star
14

gallery-rs

Rust Language Code Gallery covering a variety of fields and programming styles
Rust
1
star
15

MELIA

Clone of MELIA a theorem prover for the Model Evolution Calculus with Equality and built-in linear integer arithmetic.
Scala
1
star
16

scalafxml-demo

scalafxml-demo is a scalaFXML port of The Audio Configuration “More Cowbell” program from Pro JavaFX 2 book.
Java
1
star