awesome-rust-formalized-reasoning

awesome-rust-formalized-reasoning copied to clipboard

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

• Projects
  • Provers & Solvers
    • Provers TPTP compliant
    • SAT Solver
    • Proof assistant
    • Misc
  • Verification
    • Static Analysis & Rust verification tools
    • Misc
  • Libraries
    • Parser
    • Bindings
    • Translator
    • Misc
  • Books code
  • Programming Language
  • Kanren
  • Lambda Calculus
  • Propositional Logic
  • Unclassified
• Resources
  • Books
  • Crates keywords
  • Research Paper & Thesis
  • Demos
  • Blogs
  • Posts
  • Community

Legend

• Abandoned :skull:
• Best in Class :diamonds:
• Book implementation :book:
• Crate(s) :package:
• Crates keyword fully listed :100:
• Deleted by author :recycle:
• Exhumated :ghost:
• Inactive :zzz:
• List of resources :information_source:
• Popular :star:
• Research paper implementation :lab_coat:
• Toy project :baby_chick:
• Video :tv:
• WIP :construction:

Projects

Provers and Solvers

Provers TPTP compliant

• CoP :package: - reimplement automated theorem provers of the leanCoP family, such as leanCoP and nanoCoP.
• lazyCoP - automatic theorem prover for first-order logic with equality.
• lerna :skull: - proves theorems.
• lickety - prototype system for linear resolution with splitting.
• meancop :package::skull: - became CoP.
• Serkr :ghost: :star: - automated theorem prover for first order logic with equality.

SAT Solver

• BatSat :package::star: - solver forked from ratsat, a reimplementation of MiniSat.
• CreuSAT :star: - formally verified SAT solver verified with Creusot.
• Debug-SAT :package: - debuggable automatic theorem prover for boolean satisfiability problems (SAT).
• dpll-sat - naïve SAT solver implementing the classic DPLL algorithm.
• msat :package: - MaxSAT Solver.
• RatSat :package::package::star: - reimplementation of MiniSat.
• rsat :package: - SAT Solver.
• rust-smt-ir - provides an intermediate representation (IR) in Rust for SMT-LIB queries along with tools.
• rustsat :baby_chick: - toy Rust SAT solver.
• SATCoP - theorem prover for first-order logic based on connection tableau and SAT solving.
• Satire :package: - educational SAT solver.
• SAT-MICRO - reimplementation of the SAT-solver described in 'SAT-MICRO: petit mais costaud!'.
• scrapsat :construction: - CDCDL SAT Solver.
• screwsat :package::star: - simple CDCL SAT Solver.
• slp :package::skull: - became SolHOP.
• SolHOP :package: - aims to be a SAT and MaxSAT solver. Currently, a CDCL based SAT.
• Splr :package::diamonds::star: - modern CDCL SAT solver.
• starlit :construction: - CDCL SAT solver.
• Stevia :star: - simple (unfinished) SMT solver for QF_ABV.
• UASAT-RS - SAT solver based calculator for discrete mathematics and universal algebra.
• Varisat:package::package::package::package::package::package::package::package::star: - CDCL based SAT solver.

Proof assistant

• cobalt :construction: - a wip minimal proof assistant.
• Esther :construction: - simple automated proof assistant.
• LSTS :package::star: - proof assistant that is also a programming language.
• Noq :tv::star: - Not Coq. Simple expression transformer that is not Coq.
• Poi :package::star: - pragmatic point-free theorem prover assistant.
• qbar :package: - experimental automated theorem verifier/prover and proof assistant.

Misc

• Avalog :package::star: - experimental implementation of Avatar Logic with a Prolog-like syntax.
• Caso :package: - category Theory Solver for Commutative Diagrams.
• gpp-solver :package: - small hybrid push-pull solver/planner that has the best of both worlds.
• hoice :star: - ICE-based Constrained Horn Clause (CHC) solver.
• linear_solver :package::star: - linear solver designed to be easy to use with Rust enums.
• Logic solver :star: - logic solver.
• Mikino :package::package: - simple induction and BMC engine.
• Monotonic-Solver :package::star: - monotonic solver designed to be easy to use with Rust enum expressions.
• pocket_prover :package::package::star: - fast, brute force, automatic theorem prover for first order logic.
• reachability_solver :package: - linear reachability solver for directional edges.
• relsat-rs :baby_chick: - Experiments with provers.
• shari - the 🍣 prover.

Verification

Static Analysis & Rust verification tools

• contracts :package::star: - implements "Design By Contract" via procedural macros.
• Creusot :star: - tool for deductive verification of Rust code.
• crux-mir :star: - static simulator for Rust programs.
• cwe_checker :star: - finds vulnerable patterns in binary executables.
• electrolysis :star: - tool for formally verifying Rust programs by transpiling them into the Lean 2 theorem prover.
• Flux :star::lab_coat: - liquid types for Rust.
• Kani :star::lab_coat: - bit-precise model-checker, ensures that unsafe Rust code is actually safe.
• Loom :package::star: - concurrency permutation testing tool for Rust.
• matla - a manager for TLA+ projects.
• MIRAI :package::star: - intended to become a widely used static analysis tool for Rust.
• MirChecker :star::lab_coat: - simple static analysis tool.
• p4-analyzer - static analysis tool which checks P4 code for bugs.
• Prusti :star: - prototype verifier for Rust, built upon the the Viper verification infrastructure.
• Rudra :star::lab_coat: - static analyzer to detect common undefined behaviors in Rust programs.
• Rust static analysis/verification reading and resources :information_source: - for further reading.
• Rust verification tools :star: - collection of tools/libraries about static and dynamic verification of Rust programs.
• Rust verification tools (2021) :information_source: - list of Rust verification tools with a bias towards ‘formal methods’ tools.
• Rust verification tools list :information_source: - list of tools.
• RustHorn :lab_coat: - CHC-based Automated Verification Tool for Rust.
• RustHornBelt Library & Benchmarks :lab_coat: - support paper in preview.
• Rustproof :package::star: - compiler plugin, verification condition generator.
• Shuttle :package::star: - library for testing concurrent Rust code.
• Stateright :package::star: - model checker for implementing distributed systems.
• VeriWasm :package::star::lab_coat: - SFI verifier of Wasm binaries.
• verus :star: - verified subset of Rust for low-level systems code.
• Xori :star: - static analysis library for PE32, 32+ and shellcode.

Misc

• ArcsJs - Provable - set of ArcsJs focused tools for doing proofs on ArcsJs models.
• Bounded Registers :package::star: - high-assurance memory-mapped register interaction library.
• Chalk :package::package::package::package::package::package::package::star: - implements the Rust trait system, based on Prolog-ish logic rules.
• Charon - interface with the rustc compiler for the purpose of program verification.
• Kinō :skull: - re-implementation of the core verification engine of Kind 2 model-checker.
• Kontroli :package::package::package::tv::lab_coat::diamonds: - alternative implementation of the logical framework Dedukti.
• Metamath-knife - verify Metamath proofs.
• pocket_prover-set :package: - base logical system for PocketProver to reason about set properties.
• rate :package::package::package::package::package::diamonds: - clausal proof checker (DRAT, DPR) for certifying SAT solvers' unsatisfiability results.
• rlfsc :package: - checker for the LFSC proof language.
• second_opinion - verifier for Metamath Zero proof files.
• smetamath :package: :star: - parallel and incremental verifier for Metamath databases.
• Supervisionary :lab_coat: - experimental proof-checking system for Gordon's higher-order logic.
• t3p - optimized TESC (Theory-Extensible Sequent Calculus) verifier.
• Verifier :package: - Trivial proof verifier - an interface to the Metamath Zero kernel.

Libraries

Parser

• CNF Parser :package: - efficient and customizable parser for the .cnf file format.
• DIMACS Parser :package: - utilities to parse files in DIMACS .cnf or .sat file format.
• Flussab CNF :package: - parsing and writing of the DIMACS CNF file format.
• FRAT-rs :lab_coat: - 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 :package: - parser for the Metamath Zero binary proof format.
• olean-rs - parser/viewer for olean files.
• smt2 :package: - SMT-LIB 2 parsing library.
• tptp :package::diamonds: - parse the TPTP format.

Bindings

• boolector :package: - safe high-level bindings for the Boolector SMT solver.
• bitwuzla-sys :package: - low-level bindings for the Bitwuzla SMT solver.
• boolector-sys :package: - low-level bindings for the Boolector SMT solver.
• CaDiCaL SAT solver :package: - bindings for the CaDiCaL SAT solver.
• cryptominisat-rs :package: - bindings for CryptoMiniSat.
• falcon-z3 :package: - bindings for Z3.
• IPASIR :package: - FFI bindings for the IPASIR incremental SAT solver interface.
• Kissat-rs :package: - bindings for the Kissat SAT solver.
• lean-sys :package: - bindings to Lean 4's C API.
• libsmt.rs - bindings for SMTLIB2.
• rsmt2 :package::package::star: - generic library to interact with SMT-LIB 2 compliant solvers.
• Rust-SMT-LIB-API :package::skull::star: - generic high-level API for interacting with SMT solvers.
• rustproof-libsmt :package: - fork of libsmt.rs.
• z3 :package::package::star: - high-level and low-level Rust bindings for the Z3 solver.
• z3-rust :package: - high level bindings for the Microsoft's Z3 SMT solver.
• Z3D :package: - Z3 DSL interface.

Translator

• anthem - translate answer set programs to first-order theorem prover language.
• Cnfpack :package: - converts between DIMACS CNF file format and the compressed binary Cnfpack format.
• hz-to-mm0 - translator from HOL Zero / Common HOL to Metamath Zero.

Misc

• AbsoluteUnity - think Prolog, but less capable.
• Alice_rs :lab_coat::lab_coat: - implementation of a decision procedure for A Decidable Fragment of Separation Logic.
• Avatar Hypergraph Rewriting :package: - hypergraph rewriting system with avatars for symbolic distinction.
• coc - the calculus of constructions.
• compiler :package::baby_chick: - trivial compiler framework for Metamath Zero binary proofs.
• discrimination-tree :package: - discrimination tree term indexing.
• egg :package::star: - flexible, high-performance e-graph library.
• epilog :package: - collection of Prolog-like tools for inference logic.
• FALL :package: - easily embeddable, futures-friendly logic engine.
• Fathom :package::star: - declarative data definition language for formally specifying binary data formats.
• foliage :package: - first-order logic with integer arithmetics.
• Joker Calculus :package: - implementation of Joker Calculus in Rust.
• Kravanenn :star: - set of tools for Coq.
• LogRu :package: - small, embeddable and fast interpreter for a subset of Prolog.
• mm0-rs :package::package::package::star::lab_coat::lab_coat: - 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 :package::package::star: - automagical variable binding library.
• nanoda :skull::star: - became nanoda-lib.
• nanoda_lib - type inference/checking functionality based on the Lean theorem prover.
• polytype :package::star: - Hindley-Milner polymorphic typing system.
• program-induction :package::star: - library for program induction and learning representations.
• rust-nbe-for-mltt :star: - normalization by evaluation for Martin-Löf Type Theory with dependent records.
• rust-unify :package: :recycle: - unification algorithum implementation.
• Rusty Razor :package::package::package::star: - tool for constructing finite models for first-order theories.
• Satoxid :package: - library to help with encoding SAT problems.
• smt2utils :package::package::package::package: - libraries and tools for the SMT-LIB-2 standard.
• term-rewriting-rs :package: :star: - representing, parsing, and computing with first-order term rewriting systems.
• tribool :package: - three-valued logic.
• The Trivial Metamath Zero kernel :package: - Metamath Zero kernel for Trivial.
• Whisper :star: - logic Programming DSL.

Books code

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

• logic-rs :book::skull::star: - parser of relational predicate logic & truth tree solver
• plar-rs :book::ghost: - exploring John Harrison's Handbook of Practical Logic and Automated Reasoning.
• tapl - implementation of TAPL.
• TAPL in Rust :star: - another collection of implementations of TAPL.
• tnt :book::package: - implementation of Hofstader's "Typographical Number Theory" from the book Gödel, Escher & Bach.
• types-and-programming-languages :star: - Exercises from Benjamin Pierce's TAPL textbook + extras!

Programming Language

• egglog :star: - using the egg library with a file format and semantics similar to datalog.
• High-order Virtual Machine (HVM) :star: - massively parallel, optimal functional runtime.
• isotope-prover-experiments :construction: :lab_coat: :lab_coat: - experimental dependently typed language supporting borrow checking.
• Kind2 :package::star: - modern proof language prototype successor of Kind-Lang.
• Last Order Logic :package: - experimental logical language.
• minihl - formal methods playgorund for MiniHeapLang language.
• minitt-rs :package::package::skull::star: - became Voile.
• Narc :package::star: - dependently-typed programming language with Agda style dependent pattern matching.
• Pikelet :package::star: - small, functional, dependently typed programming language.
• proto-vulcan :package::package: - miniKanren-family relational logic programming language.
• Scryer Prolog :package::star: - modern Prolog implementation.
• Symmetric Interaction Calculus :star: - match the optimal λ-calculus reduction algorithm perfectly.
• tako - experimental programming language for ergonomic software verification.
• TIP :baby_chick: - imperative programming language aimed at teaching fundamental concepts of static program analysis.
• Untyped Concatenative Calculus - toy programming language and prototype for Dawn.
• Voile :package::package::skull::star: - became Narc.
• zz :package::skull::star: - zymbolic verifier and tranzpiler to bare metal C.

Kanren

• Canrun :package::star: - logic programming library inspired by the *Kanren family of language DSLs.
• miniKANREN :package: - miniKANREN as a DSL.
• rslogic :package::star: - logic programming framework for Rust inspired by µKanren.
• rust-kanren :star: - loose interpretation of miniKanren and cKanren.
• µKanren-rs :package::star: - implementation of µKanren.

Lambda Calculus

• blc :package: - implementation of the binary lambda calculus.
• Closure Calculus :package::lab_coat: - library for Barry Jay's Closure Calculus.
• lambda_calc :package: - command-line untyped lambda calculus interpreter.
• lambda_calculus :package::star: - simple, zero-dependency implementation of pure lambda calculus in safe Rust.
• lambda_calculus - no description.
• lambdacube :construction: - implementation of the lambda cube (and other type stuff).
• Lamcal :package::package: - lambda calculus parser and evaluator and a separate command line REPL.

Propositional logic

• Chevre :recycle: - small propositional logic interpreter.
• logic :package: :baby_chick: - crate for propositional logic.
• logic-resolver :baby_chick: - toy implementation of resolution for propositional logic.
• plc - propositional logic calculator.
• Prop :package: - library for theorem proving with Intuitionistic Propositional Logic.
• Propositional Tableaux Solver :package: - solver using the propositional tableaux method.
• Resolution Prover - resolution prover library for propositional logic.
• rs-logik :ghost: - propositional logic interpreter.
• rusty-logic :baby_chick: - propositional logic analysis.
• simple-proof-assistant :baby_chick: - 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.
• 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 :package: - 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 :star: - type-level implementation of Smallfuck in Rust. Turing-completeness proof for Rust's type system.

Resources

Books

• Verification for Dummies: SMT and Induction - broadly discusses induction as a formal verification technique.

Research Paper & Thesis

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

Demos

• Artifact Evaluation: Kani Rust Verifier :lab_coat: - Kani Rust Model Checker artifact for ICSE 2022 Artifact Evaluation.
• flux-demo - small examples that demonstrate how flux works.

Blogs

• A Formal Verification of Rust's Binary Search Implementation. :uk:
• Kani Rust Verifier Blog :uk:
• Splr notebook. :jp:
• Research notebook about improving with Rust the performance of nonclausal automated theorem provers. :uk::diamonds:
• Articles about a collection of tools/libraries to support both static and dynamic verification of Rust programs. :uk:
• Varisat notebook. :uk:

Posts

• Formally Verifying Rust's Opaque Types

Crates keywords

• solver - 81 entries. :100:
• logic - 41 entries. :100:
• verification - 27 entries. :100:
• sat - 26 entries. :100:
• smt - 26 entries. :100:
• satisfiability - 23 entries. :100:
• rewriting - 8 entries. :100:
• prover - 8 entries. :100:
• first-order - 6 entries. :100:
• cnf - 6 entries. :100:
• smt-lib - 6 entries. :100:
• metamath-zero - 5 entries. :100:
• z3 - 5 entries. :100:
• dependent-types - 5 entries. :100:
• dimacs - 5 entries. :100:

Community

• Johannes Altmanninger - rate.
• Mikko Aarnos - Serkr.
• ammkrn - nanoda, nanoda_lib, second_opinion.
• Yechan Bae - Rudra, Satire.
• Clark Barrett - Rust-SMT-LIB-API.
• Mathieu Baudet - smt2utils.
• James Bornholt - rustsat, Shuttle.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• 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.
• Eric Zhang - µKanren-rs.
• Tesla Ice Zhang - minitt-rs, Narc, Voile.
• Felix Zhu - lambdacube.
• Li Zhuohua - MirChecker.
• Philip Zucker - egglog.