A curated list of awesome rust resources regarding automated or semi-automated formalization efforts in any area, including classical mathematics, constructive mathematics formal algorithms, and program verification.
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.
- reimplement automated theorem provers of the leanCoP family, such as leanCoP and nanoCoP. - automatic theorem prover for first-order logic with equality. - proves theorems. - prototype system for linear resolution with splitting. - became CoP. - first bits for first-order logic prover. - automated theorem prover for first order logic with equality. - solver forked from ratsat, a reimplementation of MiniSat. - formally verified SAT solver verified with Creusot. - debuggable automatic theorem prover for boolean satisfiability problems (SAT). - naïve SAT solver implementing the classic DPLL algorithm. - SAT/SMT Solver. - solver of non-linear (in)equations encoded in a subset of the SMT-Lib format. - tiny DPLL SAT-solver. - experimental minisat SAT solver. - MaxSAT Solver. - CDCL SAT solver written for skill and research. - reimplementation of MiniSat. - fast package resolver (CDCL based SAT solving). - SAT Solver. - toy SAT solver. - SAT solver. - simple SAT solver. - reimplementation of the SAT-solver described in ‘SAT-MICRO: petit mais costaud!’. - theorem prover for first-order logic based on connection tableau and SAT solving. - educational SAT solver. - DPLL SAT solver. - CDCDL SAT Solver. - simple CDCL SAT Solver. - multi-objective MaxSAT solver based on the rustsat library and the CaDiCaL SAT solver. - became SolHOP. - aims to be a SAT and MaxSAT solver. Currently, a CDCL based SAT. - modern CDCL SAT solver. - CDCL SAT solver. - simple (unfinished) SMT solver for QF_ABV. - CDCL based SAT solver. - linear programming library that provides primal and dual simplex solvers. - linear programming solver (fork of minilp). - linear programming solver. - a wip minimal proof assistant. - simple automated proof assistant. - implementation of homotopy.io proof assistant. - proof assistant that is also a programming language. - An environment for learning formal mathematical reasoning from scratch. - Not Coq. Simple expression transformer that is not Coq. - pragmatic point-free theorem prover assistant. - experimental automated theorem verifier/prover and proof assistant. - experimental implementation of Avatar Logic with a Prolog-like syntax. - automatic conversion of functions to CNF for SAT solving. - profiler for exploring and visualizing SMT solver quantifier instantiations. - category Theory Solver for Commutative Diagrams. - cyclic theorem prover for equational reasoning using egraph. - Mixed Integer Linear Programming modeler using external solvers. - small hybrid push-pull solver/planner that has the best of both worlds. - ICE-based Constrained Horn Clause (CHC) solver. - multi logic theorem prover based on Graham Priests 2008 book. - linear solver designed to be easy to use with Rust enums. - logic solver. - simple induction and BMC engine. - monotonic solver designed to be easy to use with Rust enum expressions. - simple little logic solver and calculator. - fast, brute force, automatic theorem prover for first order logic. - first-order logic prover. - experiment with integer relation prover. - reimplementation of the Cosette prover in Rust. - linear reachability solver for directional edges. - Experiments with provers. - a linear programming solver based on the Simplex algorithm. - framework for manipulating SAT problems. - toolbox for analyzing performance and runtime characteristics of SAT solvers. - proof search algorithm for boolean formulae. - simple sequent solver. - automatically analyses and visualises SMT solver execution traces. - SMT library. Mainly project at the verification course in THU. - first-order conic solver for convex optimization problems . - interface with the rustc compiler for the purpose of program verification. - formal verification for Rust. - implements “Design By Contract“ via procedural macros. - tool for deductive verification of Rust code. - static simulator for Rust programs. - finds vulnerable patterns in binary executables. - tool for formally verifying Rust programs by transpiling them into the Lean 2 theorem prover. - refinement type checker for Rust. - find Deadlocks in Rust with Petri-Net Model checking. - tool for high assurance translations of a large subset of Rust into formal languages such as F* or Rocq. - bit-precise model-checker, ensures that unsafe Rust code is actually safe. - implement Liquid Types type checker. - statically detect deadlocks bugs for Rust. - concurrency permutation testing tool for Rust. - intended to become a widely used static analysis tool for Rust. - simple static analysis tool. - prototype verifier for Rust, built upon the the Viper verification infrastructure. - Realizable, Reconfigurable, Unobtrusive Unit (R2U2) stream-based runtime verification. - type system for high-assurance verification of Rust Programs. - high-performance implementation of the IC3/PDR algorithm. - static analyzer to detect common undefined behaviors in Rust programs. - collection of Rust verification benchmarks with their verifier crates. - for further reading. - verifying the Rust standard library. - collection of tools/libraries about static and dynamic verification of Rust programs. - list of Rust verification tools with a bias towards ‘formal methods’ tools. - list of tools. - CHC-based Automated Verification Tool for Rust. - evaluation libraries and benchmarks for the RustHornBelt PLDI paper. - compiler plugin, verification condition generator. - library for testing concurrent Rust code. - model checker for implementing distributed systems. - research prototype tool for modular formal verification of C, Rust and Java programs.veriwasm.pdf"> - SFI verifier of Wasm binaries. - verified subset of Rust for low-level systems code. - static analysis library for PE32, 32+ and shellcode. - high-assurance memory-mapped register interaction library. - proof checker and elaborator for SMT proofs in the Alethe format. - library for defining models in Computational Tree Logic and verifying their semantics. - implements the Rust trait system, based on Prolog-ish logic rules. - re-implementation of the core verification engine of Kind 2 model-checker. - alternative implementation of the logical framework Dedukti. - verify Metamath proofs. - Alternative Mizar proof checker. - base logical system for PocketProver to reason about set properties. - clausal proof checker (DRAT, DPR) for certifying SAT solvers’ unsatisfiability results. - checker for the LFSC proof language. - Metamath verifier. - parallel and incremental verifier for Metamath databases. - experimental proof-checking system for Gordon’s higher-order logic. - framework for temporal verification based on first-order linear-time temporal logic. - framework to build practical, formally verified, cluster management controllers. - Trivial proof verifier - an interface to the Metamath Zero kernel. - efficient and customizable parser for the .cnf file format. - utilities to parse files in DIMACS .cnf or .sat file format. - provides routines to parse SAT solver output and to execute SAT solver. - parsing and writing of the DIMACS CNF file format. - toolchain for processing and transforming files in the FRAT format. - library for representing Cube, Clause, CNF and DNF. - library for lexing, parsing and visualizing logical expressions. - LP file parser. - parser for the Metamath Zero binary proof format. - fast MPS parser. - parser/viewer for olean files. - btor2 parser, wip hardware bug-finding toolkit. - parsing and handling simple logical expressings. - SMT-LIB 2 parsing library. - parse the TPTP format. - safe high-level bindings for the Boolector SMT solver. - low-level bindings for the Bitwuzla SMT solver. - low-level bindings for the Boolector SMT solver. - bindings for the CaDiCaL SAT solver. - almost complete safe and unsafe bindings for the CaDiCal SAT solver. - bindings for the Kissat SAT solver. - idiomatic bindings to the clingo library. - safe rust bindings for CPLEX. - bindings for CryptoMiniSat. - simplified API to get started with the z3 SAT solver. - bindings for Z3. - safe rust bindings for the HiGHS linear programming solver. - bindings for the HiGHS linear programming solver. - FFI bindings for the IPASIR incremental SAT solver interface. - load shared libraries of IPASIR compatible SAT solvers. - client to interact with an Isabelle server. - bindings for the Kissat SAT solver. - bindings to Lean 4‘s C API. - bindings for SMTLIB2. - low-level LogicNG bindings for the MaxSAT solver Open-WBO. - high-level lpsolve wrapper. - bindings for the (multi-objective) MaxSAT preprocessor MaxPre. - safe bindings for pblib. - bindings for CPLEX. - generic library to interact with SMT-LIB 2 compliant solvers. - provides Rust bindings for multiple popular SAT solvers. - safe Rust interface for SCIP. - generic high-level API for interacting with SMT solvers. - use Z3 SMT solver from rust. - fork of libsmt.rs. - raw rust bindings to SCIP. - Z3 SMT Simple Binding. - high-level API for interacting with SMT solvers. - low and high-level bindings to the Yices2 SMT solver. - high-level and low-level Rust bindings for the Z3 solver. - high level bindings for the Microsoft’s Z3 SMT solver. - Z3 DSL interface. - translate answer set programs to first-order theorem prover language. - transfer boolean expression to dimacs directly. - create boolean formulae from boolean expressions and integer expressions. - converts between DIMACS CNF file format and the compressed binary Cnfpack format. - translating formulas generated by d4 into the format generated by c2d. - translator from HOL Zero / Common HOL to Metamath Zero. - intermediate representation (IR) in Rust for SMT-LIB queries. - think Prolog, but less capable. - implementation of a decision procedure for A Decidable Fragment of Separation Logic. - decision procedure for intuitionistic logic. - hypergraph rewriting system with avatars for symbolic distinction. - the calculus of constructions. - trivial compiler framework for Metamath Zero binary proofs. - discrimination tree term indexing. - easy SMT solver interaction (Inspired by the simple-smt haskell package.). - flexible, high-performance e-graph library. - collection of Prolog-like tools for inference logic. - easily embeddable, futures-friendly logic engine. - first-order logic with integer arithmetics. - provides operations and inference for fuzzy set theory. - implementation of Joker Calculus in Rust. - set of tools for Coq. - structural logic based on equivalence graphs. - library for solving and parsing logical equations. - library for creating, manipulating and solving Boolean and Pseudo-Boolean formulas. - small, embeddable and fast interpreter for a subset of Prolog. - MM0/MM1 server and utilities. - utility tools for Metamath Zero binary proof files. - library containing the definitions of the opcodes in the Metamath Zero binary proof files. - automagical variable binding library. - became nanoda-lib. - type inference/checking functionality based on the Lean theorem prover. - Negation Normal Form manipulation library. - Hindley-Milner polymorphic typing system. - library for program induction and learning representations. - rewrite rule inference using equality saturation. - syntax of First Order Logic with self-consistent logical assertions. - normalization by evaluation for Martin-Löf Type Theory with dependent records. - library for strings as defined in the SMT-LIB theory of strings. - unification algorithum implementation. - provide elements commonly used in satisfiability solving software. - tool for constructing finite models for first-order theories. - convenient way to write and solve SAT constraints. - library to help with encoding SAT problems. - libraries and tools for the SMT-LIB-2 standard. - syntactic types the for the SMT-LIB 2.6 spec. Meant for code generation, not parsing. - representing, parsing, and computing with first-order term rewriting systems. - three-valued logic. - Metamath Zero kernel for Trivial. - logic Programming DSL.There is numerous implementations of TAPL , we keep only the most popular and keep an eye on implementations that worth attention.
- parser of relational predicate logic & truth tree solver - exploring John Harrison’s Handbook of Practical Logic and Automated Reasoning. - implementation of TAPL. - collection of implementations of TAPL (Chap 3-10,17,25). - transpiled J-Bob assistant & GUI frontend. - a Rust take on D.Friedman’s book. - implementation of Hofstader’s “Typographical Number Theory” from the book Gödel, Escher & Bach. - Exercises from TAPL textbook + extras! (Chap 5-7,9-10) - language that combines the benefits of equality saturation and datalog. - declarative data definition language for formally specifying binary data formats. - massively parallel, optimal functional runtime. - programming language (fit the optimal λ-calculus reduction algorithm perfectly). - experimental dependently typed language supporting borrow checking. - next-gen functional language and proof assistant. - experimental logical language. - became Voile. - dependently-typed programming language with Agda style dependent pattern matching. - small, performance-oriented, dependently typed ML with algebraic effects and unboxed types.. - small, functional, dependently typed programming language. - miniKanren-family relational logic programming language. - a language for compiling formal mathematical models into static models. - partial re-implementation of pi-forall. - modern Prolog implementation. - Sat Modulo Theory Language. - symbolic execution engine. Mainly targeted at the verification course in THU. - programming language aimed at teaching fundamental concepts of static program analysis. - toy programming language and prototype for Dawn. - became Narc. - zymbolic verifier and tranzpiler to bare metal C. - logic programming library inspired by the *Kanren family of language DSLs. - miniKANREN as a DSL. - logic programming framework for Rust inspired by µKanren. - loose interpretation of miniKanren and cKanren. - implementation of µKanren. - implementation of the binary lambda calculus. - library for Barry Jay’s Closure Calculus. - implementation of the pure untyped lambda calculus in modern, safe Rust. - λ-calculus shell. - command-line untyped lambda calculus interpreter. - simple, zero-dependency implementation of pure lambda calculus in safe Rust. - lambda calculus with antlr grammar. - implementation of the lambda cube (and other type stuff). - simple REPL shell for untyped lambda expressions. - lambda calculus parser and evaluator and a separate command line REPL. - λ-calculus grammar/interpretor written using LALRPOP and λ!. - variant of Typed Lambda Calculus with generalized variable punning (ad-hoc polymorphism). - Overly-documented Lambda Calculus Interpreter. - typed λ-calculus. - small propositional logic interpreter. - storing logical formulas as parse trees and performing complex operations on them. - crate for propositional logic. - toy implementation of resolution for propositional logic. - reads a logical proposition and interprets it to build the truth table and the AST. - CLI tool for parsing and processing LaTex formatted propositional statements. - propositional logic calculator. - propositional logic evaluator and rule-based pattern matcher. - library for theorem proving with Intuitionistic Propositional Logic. - propositional Logic Library. - propositional logic evaluator (truth tables for propositional expressions). - solver using the propositional tableaux method. - library for working with Logical Propositions. - prover for sentences of propositional calculus. - resolution prover library for propositional logic. - Uses propositional resolution to prove statements and proofs on discord. - propositional logic interpreter. - toy language for Propositional Logic. - propositional logic analysis. - a proof assistant kernel for minimal propositional logic. - small utility to test a propositional logic theorem prover. - simulations to learn formal systems as typed first-order term rewriting systems. - runs Peano arithmetic on Rust types, verified at compile time.. - to learn typed first-order term rewriting systems that perform list routines. - tui for logical_solver. - uses a SAT solver to find minimal partial assignments that are model of a CNF formula. - modelling n-queens problem as conjunctive normal form and solving it with DPLL algorithm. - lightning fast nonogram solver. - proc-macro Coq code generation and proof automation. - solving a number of SAT problems using Z3. - investigate phase transitions in k-SAT problems. - reduction of the superpermutation problem to Quantified Boolean Formula. - attempt to find superpermutations by reducing the problem to SAT. - type-level implementation of Smallfuck. Turing-completeness proof for Rust’s type system. - chess implemented entirely in the Rust type system. - verifier for Factorio blueprints. - 2024 - Kani Rust Model Checker artifact for ICSE 2022 Artifact Evaluation.
- 2024