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.
- Archived π
- Best in Class
β¦οΈ - Book implementation π
- Crate(s) π¦
- Crates keyword fully listed π―
- Deleted by author β»οΈ
- Exhumated π»
- Inactive π€
- List of resources βΉοΈ
- Popular β
- Research paper implementation π₯Ό
- Toy project π€
- Video πΊ
- WIP π§
- 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.
- BatSat π¦β - solver forked from ratsat, a reimplementation of MiniSat.
- 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.
- msat π¦ - MaxSAT Solver.
- RatSat π¦π¦β - reimplementation of MiniSat.
- rsat π¦ - SAT Solver.
- rust-smt-ir - provides an intermediate representation (IR) in Rust for SMT-LIB queries along with tools.
- rustsat π€ - toy Rust SAT solver.
- SATCoP - theorem prover for first-order logic based on connection tableau and SAT solving.
- Satire π¦ - educational SAT solver.
- SAT-MICRO π₯Ό - reimplementation of the SAT-solver described in 'SAT-MICRO: petit mais costaud!'.
- scrapsat π§ - CDCDL SAT Solver.
- screwsat π¦β - simple CDCL 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.
- hakim - hacky interactive theorem prover.
- cobalt β»οΈπ» - a wip minimal proof assistant.
- Esther π§ - simple automated 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.
- qbar π¦ - experimental automated theorem verifier/prover and proof assistant.
- 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.
- 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.
- Sequent solver π€ - simple sequent solver.
- shari - the π£ prover.
- 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 βπ₯Ό - liquid types for Rust.
- Kani βπ₯Ό - bit-precise model-checker, ensures that unsafe Rust code is actually safe.
- 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 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 π₯Ό - support paper in preview.
- 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.
- ArcsJs - Provable - set of ArcsJs focused tools for doing proofs on ArcsJs models.
- Bounded Registers π¦β - high-assurance memory-mapped register interaction library.
- 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.
- 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.
- Verifier π¦ - Trivial proof verifier - an interface to the Metamath Zero kernel.
- CNF Parser π¦ - efficient and customizable parser for the .cnf file format.
- DIMACS Parser π¦ - utilities to parse files in DIMACS .cnf or .sat file format.
- Flussab CNF π¦ - parsing and writing of the DIMACS CNF file format.
- FRAT-rs π₯Ό - toolchain for processing and transforming files in the FRAT format.
- Lambda Term Parsing - explores different parser designs for a simple lambda term grammar.
- mmb-parser π¦ - parser for the Metamath Zero binary proof format.
- olean-rs - parser/viewer for olean files.
- smt2 π¦ - SMT-LIB 2 parsing library.
- tptp π¦
β¦οΈ - parse the TPTP format.
- 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 SAT solver π¦ - bindings for the CaDiCaL SAT solver.
- cryptominisat-rs π¦ - bindings for CryptoMiniSat.
- falcon-z3 π¦ - bindings for Z3.
- IPASIR π¦ - FFI bindings for the IPASIR incremental SAT solver interface.
- Kissat-rs π¦ - bindings for the Kissat SAT solver.
- lean-sys π¦ - bindings to Lean 4's C API.
- libsmt.rs - bindings for SMTLIB2.
- rsmt2 π¦π¦β - generic library to interact with SMT-LIB 2 compliant solvers.
- Rust-SMT-LIB-API π¦πβ - generic high-level API for interacting with SMT solvers.
- rustproof-libsmt π¦ - fork of libsmt.rs.
- 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.
- anthem - translate answer set programs to first-order theorem prover language.
- 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.
- AbsoluteUnity - think Prolog, but less capable.
- Alice_rs π₯Όπ₯Ό - implementation of a decision procedure for A Decidable Fragment of Separation 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.
- egg π¦β - flexible, high-performance e-graph library.
- epilog π¦ - collection of Prolog-like tools for inference logic.
- FALL π¦ - easily embeddable, futures-friendly logic engine.
- Fathom π¦β - declarative data definition language for formally specifying binary data formats.
- foliage π¦ - first-order logic with integer arithmetics.
- Joker Calculus π¦ - implementation of Joker Calculus in Rust.
- Kravanenn β - set of tools for Coq.
- 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.
- polytype π¦β - Hindley-Milner polymorphic typing system.
- program-induction π¦β - library for program induction and learning representations.
- 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.
- Satoxid π¦ - library to help with encoding SAT problems.
- smt2utils π¦π¦π¦π¦ - libraries and tools for the SMT-LIB-2 standard.
- 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.
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!
- egglog β - using the egg library with a file format and semantics similar to datalog.
- High-order Virtual Machine (HVM) β - massively parallel, optimal functional runtime.
- isotope-prover-experiments π§ π₯Ό π₯Ό - experimental dependently typed language supporting borrow checking.
- Kind2 π¦β - modern proof language prototype successor of Kind-Lang.
- 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.
- Pikelet π¦β - small, functional, dependently typed programming language.
- proto-vulcan π¦π¦ - miniKanren-family relational logic programming language.
- Scryer Prolog π¦β - modern Prolog implementation.
- Symmetric Interaction Calculus β - match the optimal Ξ»-calculus reduction algorithm perfectly.
- 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.
- Voile π¦π¦πβ - became Narc.
- zz π¦πβ - zymbolic verifier and tranzpiler to bare metal C.
- 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.
- blc π¦ - implementation of the binary lambda calculus.
- Closure Calculus π¦π₯Ό - library for Barry Jay's Closure Calculus.
- lambda_calc π¦ - command-line untyped lambda calculus interpreter.
- lambda_calculus π¦β - simple, zero-dependency implementation of pure lambda calculus in safe Rust.
- lambda_calculus - no description.
- lambdacube π§ - implementation of the lambda cube (and other type stuff).
- Lamcal π¦π¦ - lambda calculus parser and evaluator and a separate command line REPL.
- Chevre β»οΈ - small propositional logic interpreter.
- logic π¦ π€ - crate for propositional logic.
- logic-resolver π€ - toy implementation of resolution for propositional logic.
- plc - propositional logic calculator.
- Prop π¦ - library for theorem proving with Intuitionistic Propositional Logic.
- Propositional Tableaux Solver π¦ - solver using the propositional tableaux method.
- 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.
- 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.
- formal-systems-learning-rs - simulations to learn formal systems as typed first-order term rewriting systems.
- list-routine-learning-rs - simulations to learn typed first-order term rewriting systems that perform list routines.
- 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.
- rummy_to_sat - implementation of a solver for Rummy.
- 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 in Rust. Turing-completeness proof for Rust's type system.
- Verification for Dummies: SMT and Induction - broadly discusses induction as a formal verification technique.
- 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.
- Artifact Evaluation: Kani Rust Verifier π₯Ό - Kani Rust Model Checker artifact for ICSE 2022 Artifact Evaluation.
- flux-demo - small examples that demonstrate how flux works.
- A Formal Verification of Rust's Binary Search Implementation. π¬π§
- Kani Rust Verifier 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. π¬π§
- solver - 81 entries. π―
- logic - 41 entries. π―
- verification - 27 entries. π―
- sat - 26 entries. π―
- smt - 26 entries. π―
- satisfiability - 23 entries. π―
- linear-programming - 11 entries.
- rewriting - 8 entries. π―
- prover - 8 entries. π―
- first-order - 6 entries. π―
- cnf - 6 entries. π―
- smt-lib - 6 entries. π―
- metamath-zero - 5 entries. π―
- z3 - 5 entries. π―
- dependent-types - 5 entries. π―
- dimacs - 5 entries. π―
- Johannes Altmanninger - rate.
- Mikko Aarnos - Serkr.
- ammkrn - nanoda, nanoda_lib, second_opinion.
- arbaregni - resolution-prover.
- Yechan Bae - Rudra, Satire.
- Clark Barrett - Rust-SMT-LIB-API.
- Mathieu Baudet - smt2utils.
- James Bornholt - rustsat, Shuttle.
- Bickio O'Callahan - Solving The Witness with Z3.
- Mario Carneiro - FRAT-rs, hz-to-mm0, mm0-rs, olean-rs, smetamath.
- Adrien Champion - hoice, KinΕ, matla, Mikino, rsmt2, SAT-MICRO, Verification for Dummies.
- Michelle Cheatham - rusty-logic.
- Alex Chew - Z3D.
- Simon Cruanes - BatSat.
- Dacit - Sequent solver.
- Ariel Davis - coc.
- Xavier Denis - Creusot, RustHornBelt Library & Benchmarks, Rust verification tools (2021).
- Sushant Dinesh - libsmt.rs.
- Craig Disselkoen - boolector.
- Mark Drobnak - p4-analyzer.
- Bruno Dutertre - rust-smt-ir.
- Thomas Dziedzic - lambda_calculus.
- 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.
- FireFighterDuck - Alice_rs, Kissat-rs, minihl.
- Robin Freyler - CNF Parser, DIMACS Parser, Stevia.
- Galois, Inc. - crux-mir.
- Jad Ghalayini - isotope-prover-experiments, lean-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.
- TimothΓ©e Haudebourg - smt2.
- Son HO - Charon.
- Sarek HΓΈverstad SkotΓ₯m - CreuSAT.
- Tero Huttunen - proto-vulcan.
- Ranjit Jhala - flux-demo.
- Andrew Johnson - LSTS.
- Evan Johnson - VeriWasm.
- Dylan R. Johnston - Formally Verifying Rust's Opaque Types.
- Ralf Jung - Understanding and Evolving the Rust Programming Language.
- Hosein Kalbasi - akim.
- karroffel - contracts.
- Prateek Kumar - msat, rsat, slp, SolHOP.
- Alexey Kutepov - Noq.
- Ivan Ladelshchikov - nonogrid.
- Andrea Lattuada - verus.
- lcnr - cobalt.
- Shea Leffler - tarpit-rs, whisper.
- Nico Lehmann - Flux.
- Carl Lerche - Loom.
- ljedrz - blc, lambda_calculus.
- Patrick LΓΌhne - anthem, foliage.
- Michael Madden - Xori.
- Scott J Maddox - Untyped Concatenative Calculus.
- Harald Maida - Lamcal.
- Krzysztof MaΕysa - prover.
- Miklos Maroti - cadical-rs, relsat-rs, uasat-rs.
- Niko Matsakis - Chalk, Kani, plar-rs.
- Yusuke Matsushita - Extensible Functional-Correctness Verification of Rust Programs by the Technique of Prophecy, RustHorn.
- mbillingr - The Little Prover, the-little-typer.
- mcmfb - lambda_calc.
- Bruce Mitchener - z3.
- Lucas Morales - polytype, program-induction.
- Dominic Mulligan - Supervisionary.
- Jon Nadal - Stateright.
- 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.
- Alex Ozdemir - rlfsc.
- Chris Patuzzo - Supermux, Supersat.
- Pierre-Marie PΓ©drot - Kravanenn.
- Arvid E. Picciani - zz.
- Dan Pittman - Bounded Registers.
- Nadia Polikarpova - cyclegg.
- Christian Poveda - Chevre.
- Joshua Pratt - ArcsJs - Provable, tako.
- 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 verification tools ,Rust verification tools list.
- Nathan Ringo - FALL.
- Erik Rohkohl - n-queens-sat.
- Marco Concetto Rudilosso - validator.
- Josh Rule - formal-systems-learning-rs, list-routine-learning-rs, term-rewriting-rs.
- Salman Saghafi - Rusty Razor.
- Michael Salter - Rustproof, rustproof-libsmt.
- Ryan Schroeder - AbsoluteUnity, epilog.
- Carol Schulze - gpp-solver.
- skbaek - t3p.
- Narazaki Shuji - Splr, Splr notebook, sudoku_sat.
- snsinfu - dpll-sat.
- Mikhail Solovev - bitwuzla-sys, boolector-sys.
- SymmetricChaos - tnt.
- Victor Taelin - High-order Virtual Machine (HVM), Kind2, Symmetric Interaction Calculus..
- 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).
- Shuxian Wang - Cosette Prover.
- David A. Wheeler - Metamath-knife.
- Max Willsey - egg.
- Ivo Wingelaar - compiler, mmb-binutils, mmb-parser, mmb-types, The Trivial Metamath Zero kernel, Verifier.
- Jieyou Xu - Propositional Tableaux Solver.
- Brendan Zabarauskas - Fathom, moniker, Pikelet, rust-nbe-for-mltt.
- Alexey Zatelepin - minilp.
- Eric Zhang - Β΅Kanren-rs.
- Tesla Ice Zhang - minitt-rs, Narc, Voile.
- Felix Zhu - lambdacube.
- Li Zhuohua - MirChecker.
- Philip Zucker - egglog.