GitHub - newca12/awesome-rust-formalized-reasoning: An exhaustive list of all Ru...

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.

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

• Abandoned
• Toy project
• List of resources
• More than one crate
• Best in Class
• Popular
• Exhumated
• Deleted

Projects

Provers and Solvers

• Avalog - experimental implementation of Avatar Logic with a Prolog-like syntax.
• Debug-SAT - debuggable automatic theorem prover for boolean satisfiability problems (SAT).
• CoP - reimplement in Rust several automated theorem provers of the leanCoP family, such as leanCoP and nanoCoP.
• egglog - Using the egg library with a file format and semantics similar to datalog.
• lazyCoP - automatic theorem prover for first-order logic with equality.
• lapjv - linear Assignmment Problem solver using Jonker-Volgenant algorithm.
• lerna - proves theorems.
• Logic solver - Logic solver.
• meancop - became CoP.
• Monotonic-Solver - monotonic solver designed to be easy to use with Rust enum expressions.
• msat - MaxSAT Solver.
• OpenZKP Stark - implementation of STARK zero-knowledge-proofs.
• pocket_prover - fast, brute force, automatic theorem prover for first order logic.
• Poi - pragmatic point-free theorem prover assistant.
• RatSat - reimplementation of MiniSat.
• reachability_solver - linear reachability solver for directional edges.
• Resolution Prover - resolution prover library for propositional logic.
• rsat - SAT Solver.
• SATCoP - theorem prover for first-order logic based on connection tableau and SAT solving.
• Serkr - automated theorem prover for first order logic with equality.
• slp - became SolHOP.
• SolHOP - aims to be a SAT and MaxSAT solver. Currently, a CDCL based SAT.
• UASAT-RS - SAT solver based calculator for discrete mathematics and universal algebra.
• Varisat - CDCL based SAT solver.
• Winterfell - A STARK prover and verifier for arbitrary computations.

Verification

• Bounded Registers - high-assurance memory-mapped register interaction library.
• CaDiCaL SAT solver - bindings for the CaDiCaL SAT solver.
• Chalk - implements the Rust trait system, based on Prolog-ish logic rules.
• Chevre - small propositional logic interpreter.
• Creusot - tool for deductive verification of Rust code.
• crux-mir - static simulator for Rust programs. It runs a set of test cases and attempts to prove that all assertions pass on all valid inputs.
• frat-rs - verify DIMACS proof.
• Kontroli - alternative implementation of the logical framework Dedukti, concentrating on the verification of proofs.
• p4-analyzer - static analysis tool which checks P4 code for bugs.
• pocket_prover-set - base logical system for PocketProver to reason about set properties.
• Prusti - prototype verifier for Rust, built upon the the Viper verification infrastructure.
• rate - clausal proof checker (DRAT, DPR) for certifying SAT solvers' unsatisfiability results.
• rlfsc - A checker for the LFSC proof language.
• Rust verification tools list - list of tools
• smetamath - parallel and incremental verifier for Metamath databases.
• Scryer Prolog - modern Prolog implementation.
• t3p - optimized TESC (Theory-Extensible Sequent Calculus) verifier.
• Verifier - Trivial proof verifier - an interface to the Metamath Zero kernel.

Libraries

• anthem - translate answer set programs to first-order theorem prover language.
• Closure Calculus - library for Barry Jay's Closure Calculus.
• CNF Parser - efficient and customizable parser for the .cnf file format.
• compiler - trivial compiler framework for Metamath Zero binary proofs.
• DIMACS Parser - utilities to parse files in DIMACS .cnf or .sat file format.
• discrimination-tree - discrimination tree term indexing.
• egg - flexible, high-performance e-graph library.
• Fathom - declarative data definition language for formally specifying binary data formats.
• Flussab CNF - parsing and writing of the DIMACS CNF file format
• foliage - first-order logic with integer arithmetics.
• formal-systems-learning-rs - simulations using 2AFC triads to learn formal systems as typed first-order term rewriting systems.
• Kravanenn - set of tools for Coq.
• linear_solver - linear solver designed to be easy to use with Rust enums.
• list-routine-learning-rs - simulations using input/output examples to learn typed first-order term rewriting systems that perform list routines.
• logic-rs - parser of relational predicate logic & truth tree solver.
• minitt-rs - became Voile.
• mm0-rs - MM0/MM1 server and utilities.
• mmb-binutils - utility tools for Metamath Zero binary proof files.
• mmb-parser - parser for the Metamath Zero binary proof format
• mmb-types - library containing the definitions of the opcodes in the Metamath Zero binary proof files.
• moniker - automagical variable binding library.
• n-queens-sat - Modelling n-queens problem as conjunctive normal form and solving it with DPLL algorithm.
• nanoda - became nanoda-lib.
• nanoda_lib - type inference/checking functionality based on the Lean theorem prover.
• Narc - dependently-typed programming language with Agda style dependent pattern matching.
• olean-rs - parser/viewer for olean files.
• Pikelet - small, functional, dependently typed programming language.
• polytype - Hindley-Milner polymorphic typing system.
• program-induction - library for program induction and learning representations.
• Prop - library for theorem proving with Intuitionistic Propositional Logic.
• rust-nbe-for-mltt - normalization by evaluation for Martin-Löf Type Theory with dependent records.
• rust-unify - unification algorithum implementation.
• Rusty Razor - tool for constructing finite models for first-order theories.
• Splr - modern CDCL SAT solver.
• sudoku_sat - solve Sudoku variants with SAT solvers.
• Symmetric Interaction Calculus - programming language and model of computation that matches the optimal λ-calculus reduction algorithm perfectly.
• tarpit-rs - type-level implementation of Smallfuck in Rust, doubling as a Turing-completeness proof for Rust's type system.
• term-rewriting-rs - library for representing, parsing, and computing with first-order term rewriting systems.
• tptp - parse the TPTP format.
• The Trivial Metamath Zero kernel - Metamath Zero kernel for Trivial.
• Voile - became Narc.
• Whisper - logic Programming DSL.

Books

• plar-rs - Exploring John Harrison's Handbook of Practical Logic and Automated Reasoning.
• TAPL in Rust - another collection of implementations of TAPL.
• tapl-rust - very limited TAPL implemention.
• tnt - implementation of Hofstader's "Typographical Number Theory" from the book Gödel, Escher, and Bach.
• types-and-programming-languages - Exercises from Benjamin Pierce's "Types and Programming Languages" textbook + extras!

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.

Lambda_Calculus

• blc - implementation of the binary lambda calculus.
• lambda_calc - command-line untyped lambda calculus interpreter.
• lambda_calculus - simple, zero-dependency implementation of pure lambda calculus in safe Rust.
• Lamcal - Lambda Calculus parser and evaluator and a separate command line REPL.

Resources

Thesis

Crates keywords

• solver - 60 entries.
• logic - 35 entries.
• sat - 24 entries.
• smt - 21 entries.
• satisfiability - 21 entries.
• verification - 20 entries.
• prover - 7 entries.
• rewriting - 7 entries.
• first-order - 6 entries.
• cnf - 5 entries.
• metamath-zero - 5 entries.
• dependent-types - 4 entries.
• stark - 4 entries.
• dimacs - 3 entries.

Community

• Johannes Altmanninger - rate.
• ammkrn - anoda, anoda_lib.
• Mikko Aarnos - Serkr.
• Remco Bloemen - OpenZKP Stark.
• Mario Carneiro - frat-rs, mm0-rs, olean-rs, smetamath.
• Xavier Denis - Creusot.
• Mark Drobnak - p4-analyzer.
• Andrii Dmytrenko - lapjv.
• Michael Färber - CoP, Kontroli, meancop.
• Robin Freyler - CNF Parser, DIMACS Parser.
• Galois, Inc. - crux-mir.
• Masaki Hara - Logic solver, RatSat.
• Jannis Harder - Flussab CNF, Varisat.
• Irakliy Khaburzaniya - Winterfell.
• Ilya Klyuchnikov - tapl-rust.
• Prateek Kumar - msat, rsat, slp, SolHOP.
• ljedrz - blc, lambda_calculus.
• Shea Leffler - tarpit-rs, whisper.
• Patrick Lühne - anthem, foliage.
• mcmfb - lambda_calc.
• Victor Maia - Symmetric Interaction Calculus.
• Miklos Maroti - cadical-rs, uasat-rs.
• Niko Matsakis - Chalk, plar-rs
• Harald Maida - Lamcal
• Lucas Morales - polytype, program-induction.
• Sven Nilsen - Avalog, Debug-SAT, linear_solver, Monotonic-Solver, pocket_prover, pocket_prover-set, Poi, Prop, reachability_solver.
• Alex Ozdemir - rlfsc.
• Pierre-Marie Pédrot - Kravanenn.
• Dan Pittman - Bounded Registers.
• Christian Poveda - Chevre.
• Michael Rawson - discrimination-tree, lazyCoP, lerna, SATCoP, tptp.
• Alastair Reid - Rust verification tools list.
• Erik Rohkohl - n-queens-sat.
• Josh Rule - formal-systems-learning-rs, list-routine-learning-rs, term-rewriting-rs.
• Salman Saghafi - Rusty Razor.
• skbaek - t3p.
• Narazaki Shuji - Splr, sudoku_sat.
• SymmetricChaos - tnt.
• Mark Thom - Scryer Prolog.
• Sebastian Ullrich - A Formal Verification of Rust's Binary Search Implementation, Simple Verification of Rust Programs via Functional Purification.
• Max Willsey - egg.
• Ivo Wingelaar - compiler, mmb-binutils, mmb-parser, mmb-types, The Trivial Metamath Zero kernel, Verifier.
• Brendan Zabarauskas - Fathom, moniker, Pikelet, rust-nbe-for-mltt.
• Tesla Ice Zhang - minitt-rs, Narc, Voile.
• Philip Zucker - egglog.