newca12/awesome-rust-formalized-reasoning — Gitpedia

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.

Projects
Resources
- Books
- Crates keywords
- Research Paper & Thesis
- Demos
- Blogs
- Posts
- Community

Legend

Actively maintened :fire:
Announcement :loudspeaker:
Archived :skull:
Benchmark :watch:
Best in Class :diamonds:
Book implementation :book:
Crate(s) :package:
Crates keyword fully listed :100:
Deleted by author :recycle:
Educational project :mortar_board:
Exhumated :ghost:
Inactive :zzz:
List of resources :information_source:
Paper with code :factory:
Popular :star:
Research paper :lab_coat:
Toy project :baby_chick:
Vibe coding :robot:
Video :tv:
Web demo :eyes:
WIP :construction:

Projects

Provers and Solvers

Provers TPTP compliant

CoP :package: - reimplement automated theorem provers of the leanCoP family, such as leanCoP and nanoCoP.
HopCoP - theorem prover for first-order logic based on connection tableaux and backjumping.
lazyCoP :watch::zzz: - automatic theorem prover for first-order logic with equality.
lerna :skull: - proves theorems.
lickety :zzz: - prototype system for linear resolution with splitting.
meancop :package::recycle: - became CoP.
mrs :package::package::package::package::package::package::package::package::package::package::robot::construction: - automated theorem prover using superposition calculus.
res-rs :construction: - first bits for first-order logic prover.
Serkr :star::ghost: - automated theorem prover for first order logic with equality.
theorem-prover-rs - rewrite of theorem-prover-kt a sequent-style automated theorem prover.

SAT Solver

backdoor-solver - backdoor-based SAT solver.
BatSat :package::star: - solver forked from ratsat, a reimplementation of MiniSat.
Colombini-SAT - simple 3-SAT solver.
CreuSAT :star: - formally verified SAT solver verified with Creusot.
Debug-SAT :package::zzz: - debuggable automatic theorem prover for boolean satisfiability problems (SAT).
dpll-sat :zzz: - naïve SAT solver implementing the classic DPLL algorithm.
DRSAT - Daniel's Rusty SAT solver.
logiq :package: - a Domain-Specific Language for SAT Solving and a solver using advanced SAT solving algorithms.
lutrix :zzz: - SAT/SMT Solver.
m2cSMT :package: - solver of non-linear (in)equations encoded in a subset of the SMT-Lib format.
microsat :package: - tiny DPLL SAT-solver.
minisat-rust :star::zzz: - experimental minisat SAT solver.
msat :package::skull: - MaxSAT Solver.
NanoSAT :construction: - almost-efficient implementation of the Conflit-Driven Clause Learning (CDCL) framework.
otter_sat :package: - CDCL SAT solver written for skill and research.
OxiZ :package::package::package::package::package::package::package::package::package::loudspeaker::diamonds: - this project reimplements Z3.
RatSat :package::package::star::zzz: - reimplementation of MiniSat.
Resolvo :package::star: - fast package resolver (CDCL based SAT solving).
rsat :package::skull: - 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(2) :baby_chick::zzz: - toy SAT solver.
sat - simple CDCL sat solver.
~~satsol~~ :recycle::baby_chick: - some SAT solving algorithms for DIMACS inputs.
SAT solver :baby_chick::zzz: - SAT solver.
SAT Solver(2) :baby_chick: - simple SAT solver.
SAT-MICRO :lab_coat: - reimplementation of the SAT-solver described in 'SAT-MICRO: petit mais costaud!'.
sat-solver - simple CDCL SAT solver based on the lecture 185.A93 Formal Methods in CS at TU Wien.
SAT-Solver - DPLL and CDCL Solver.
SATCoP :zzz: - theorem prover for first-order logic based on connection tableau and SAT solving.
Satire :package::zzz: - educational SAT solver.
satyrs :mortar_board::zzz: - DPLL SAT solver.
scrapsat :zzz: - CDCDL SAT Solver.
screwsat :package::star: - simple CDCL SAT Solver.
Scuttle :package::package: - multi-objective MaxSAT solver based on the rustsat library and the CaDiCaL SAT solver.
simple-sat - one of the SAT solvers of all time.
~~slp~~ :package::recycle: - became SolHOP.
SolHOP :package::skull: - aims to be a SAT and MaxSAT solver. Currently, a CDCL based SAT.
Splr :package::diamonds::star: - modern CDCL SAT solver.
StalmarckSAT :package: - SAT solver based on the Stålmarck Procedure.
starlit :construction: - CDCL SAT solver.
Stevia :star::zzz: - 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.

Solver MPS compliant

ellp :package::construction: - linear programming library that provides primal and dual simplex solvers.
microlp :package: - linear programming solver (fork of minilp).
minilp :package::star::skull: - linear programming solver.

Proof assistant

Acorn :star: - theorem prover with built-in AI assistant.
Canonical :lab_coat::tv::tv::diamonds::star: - solver for type inhabitation in dependent type theory.
~~cobalt~~ :recycle::ghost: - a wip minimal proof assistant.
Croof :star: - simple math proof tool for simple math expressions.
Esther :zzz: - simple automated proof assistant.
hakim - hacky interactive theorem prover.
homotopy-rs :lab_coat::lab_coat::diamonds::star: - implementation of homotopy.io proof assistant.
LSTS :package::star: - proof assistant that is also a programming language.
minimo :lab_coat::lab_coat::diamonds::star: - An environment for learning formal mathematical reasoning from scratch.
nnoq - simple theorem prover (nay, verifier) based on functional expression rewriting.
Noq :tv::star: - Not Coq. Simple expression transformer that is not Coq.
nyaya - proof language based on sequent calculus and Metamath.
OxiLean :package::package::package::package::package::package::package::package::package::package::package::package::robot: - theorem prover & dependent type checker inspired by Lean 4.
Poi :package::star: - pragmatic point-free theorem prover assistant.
Proost - simple proof assistant.
qbar :package::zzz: - experimental automated theorem verifier/prover and proof assistant.
shari - proof assistant based on the internal language of topos with NNO (intuitionistic higher-order arithmetic).
watson - a proof assistant with an extensible syntax system and Lua-based tactics.

Misc

Avalog :package::star: - experimental implementation of Avatar Logic with a Prolog-like syntax.
autosat :package::baby_chick: - automatic conversion of functions to CNF for SAT solving.
Axiom Profiler 2.0 :lab_coat::star: - profiler for exploring and visualizing SMT solver quantifier instantiations.
bootfrost - automated theorem proving program for first-order formulas with extensions.
Caso :package: - category Theory Solver for Commutative Diagrams.
cyclegg:star: - cyclic theorem prover for equational reasoning using egraph.
good_lp :star: - Mixed Integer Linear Programming modeler using external solvers.
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.
INCL Automated Theorem Prover :book::eyes: - multi logic theorem prover based on Graham Priests 2008 book.
linear_solver :package::star: - linear solver designed to be easy to use with Rust enums.
Logic solver :star::zzz: - logic solver.
lolli :package::package::package::package::package::package::package: - linear logic workbench: parse, prove, extract, and compile linear logic to Rust.
Mikino :package::package: - simple induction and BMC engine.
Monotonic-Solver :package::star: - monotonic solver designed to be easy to use with Rust enum expressions.
Obvious :zzz: - simple little logic solver and calculator.
pocket_prover :package::package::star: - fast, brute force, automatic theorem prover for first order logic.
prover :skull: - first-order logic prover.
prover(2) :baby_chick::zzz: - experiment with integer relation prover.
QED Prover :star::lab_coat: - reimplementation of the Cosette prover in Rust.
reachability_solver :package: - linear reachability solver for directional edges.
relsat-rs :baby_chick: - Experiments with provers.
Rustplex :package: - a linear programming solver based on the Simplex algorithm.
SAT-bench - benchmark suit for SAT solvers.
sat_lab :baby_chick::construction: - framework for manipulating SAT problems.
SAT solver ANalyser :construction: - toolbox for analyzing performance and runtime characteristics of SAT solvers.
scalop :package: - argumentation solver.
sequentprover :baby_chick: - proof search algorithm for boolean formulae.
Sequent solver :baby_chick::zzz: - simple sequent solver.
SMTSCOPE :package::star: - automatically analyses and visualises SMT solver execution traces.
stupid-smt :baby_chick::zzz: - 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 - implementation of a theorem prover for first-order logic.
Totsu :package::package::package::package::package::star: - first-order conic solver for convex optimization problems .

Verification

Static Analysis & Rust verification tools/framework

::formally :package::package::package::package::package::package::construction: - extensible toolchain for building formal methods tools and applications.
Charon :star::lab_coat::fire: - interface with the rustc compiler for the purpose of program verification.
contracts :package::star: - implements "Design By Contract" via procedural macros.
Creusot :star::fire: - tool for deductive verification of Rust code.
crux-mir :star::lab_coat: - static simulator for Rust programs.
cwe_checker :star: - finds vulnerable patterns in binary executables.
electrolysis :star::zzz: - tool for formally verifying Rust programs by transpiling them into the Lean 2 theorem prover.
Flux :tv::star::lab_coat::fire: - refinement type checker for Rust.
Granite :star::lab_coat::zzz: - find Deadlocks in Rust with Petri-Net Model checking.
Hax :package::star::lab_coat: - tool for high assurance translations of a large subset of Rust into formal languages (F*, Rocq, ...).
Kani :package::star::lab_coat::fire: - bit-precise model-checker, ensures that unsafe Rust code is actually safe.
Liquid Rust :star::zzz: - implement Liquid Types type checker.
lockbud :star::lab_coat: - statically detect deadlocks bugs for Rust.
Logically Qualified Data Types - implementation of liquid types on an implicitly-typed variant of ML.
Loom :package::star: - concurrency permutation testing tool for Rust.
Machine-check :package::package::package::package::package::package::package::package::package::package::package: - formal verification tool for digital systems.
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 :package::package::package::package::star::fire: - prototype verifier for Rust, built upon the the Viper verification infrastructure.
r2u2_core :package::lab_coat: - Realizable, Reconfigurable, Unobtrusive Unit (R2U2) stream-based runtime verification.
RefinedRust :lab_coat: - type system for high-assurance verification of Rust Programs.
rIC3 Hardware Model Checker :package::watch::star: - high-performance implementation of the IC3/PDR algorithm.
rocq-of-rust :star: - formal verification for Rust.
Rudra :star::lab_coat: - static analyzer to detect common undefined behaviors in Rust programs.
Rust Software Verification Benchmarks :zzz: - collection of Rust verification benchmarks with their verifier crates.
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 :star::lab_coat: - CHC-based Automated Verification Tool for Rust.
RustHornBelt Library & Benchmarks :lab_coat: - evaluation libraries and benchmarks for the RustHornBelt PLDI paper.
Rustproof :package::star::zzz: - compiler plugin, verification condition generator.
Shuttle :package::star: - library for testing concurrent Rust code.
Stateright :package::star: - model checker for implementing distributed systems.
VeriFast :star: - research prototype tool for modular formal verification of C, Rust and Java programs.
VeriWasm :package::star::lab_coat: - SFI verifier of Wasm binaries.
verus :star::fire::tv::lab_coat: - verified subset of Rust for low-level systems code.
vostd - formal verification of Asterinas OSTD with Verus.
Xori :star::zzz: - static analysis library for PE32, 32+ and shellcode.

Formally verified

Rust standard library verification :tv::star: - verifying the Rust standard library.
verdict :package::lab_coat::watch: - end-to-end formally verified X.509 certificate validation library.
verified-memory-allocator:star: - a memory allocator verified with Verus.
vest :package::star::lab_coat: - high-assurance and performant parsing and serialization of binary data formats verified in Verus.

Misc

ArcsJs - Provable - set of ArcsJs focused tools for doing proofs on ArcsJs models.
AutoVerus: Verus Proof Synthesis:star::lab_coat: - code and artifacts for automated Verus proof synthesis.
Bounded Registers :package::star: - high-assurance memory-mapped register interaction library.
Carcara :star::lab_coat: - proof checker and elaborator for SMT proofs in the Alethe format.
ceetle :package::package: - library for defining models in Computational Tree Logic and verifying their semantics.
Chalk :package::package::package::package::package::package::package::star: - implements the Rust trait system, based on Prolog-ish logic rules.
Kinō :skull: - re-implementation of the core verification engine of Kind 2 model-checker.
Kontroli :package::package::package::star::diamonds::tv::lab_coat: - alternative implementation of the logical framework Dedukti.
lean-tui :package: - standalone TUI infoview for Lean 4 theorem prover.
Legalis-RS :package: - formal verification for Legalis-RS legal statutes.
Metamath-knife :package::star: - verify Metamath proofs.
Mist - userfriendly verification frontend language.
Mizar proof checker :star: - Alternative Mizar proof checker.
pocket_prover-set :package: - base logical system for PocketProver to reason about set properties.
rate :package::package::package::package::package::diamonds::lab_coat: - clausal proof checker (DRAT, DPR) for certifying SAT solvers' unsatisfiability results.
rlfsc :package::zzz: - checker for the LFSC proof language.
rust-metamath :zzz: - Metamath verifier.
second_opinion - verifier for Metamath Zero proof files.
smetamath :package::star::zzz: - parallel and incremental verifier for Metamath databases.
Supervisionary :tv::lab_coat: - experimental proof-checking system for Gordon's higher-order logic.
t3p - optimized TESC (Theory-Extensible Sequent Calculus) verifier.
Temporal Verifier :star: - framework for temporal verification based on first-order linear-time temporal logic.
verifiable-controllers :star: - framework to build practical, formally verified, cluster management controllers.
Verifier :package::zzz: - Trivial proof verifier - an interface to the Metamath Zero kernel.

Libraries

Parser

CNF Parser :package::zzz: - efficient and customizable parser for the .cnf file format.
coq-rs - this program can parse Coq .vo files.
DIMACS Parser :package: - utilities to parse files in DIMACS .cnf or .sat file format.
Exec-SAT :package::baby_chick: - provides routines to parse SAT solver output and to execute SAT solver.
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.
isabelle export tool - parser for isabelle database files.
Lambda Calculus Parser - λ-calculus parser.
Lambda Term Parsing - explores different parser designs for a simple lambda term grammar.
logic-form :package::baby_chick: - library for representing Cube, Clause, CNF and DNF.
logic-parser :package::mortar_board: - library for lexing, parsing and visualizing logical expressions.
lp_parser_rs :package: - LP file parser.
mmb-parser :package: - parser for the Metamath Zero binary proof format.
mps :package: - fast MPS parser.
mrs-tptp :package: :robot::diamonds: - high performance full featured TPTP parser.
olean-rs :zzz: - parser/viewer for olean files.
Patronus :package::construction: - btor2 parser, wip hardware bug-finding toolkit.
RustLogic :package: - parsing and handling simple logical expressings.
smt-str :package: - data structures and utilities to parse, manipulate, and reason about SMT-LIB strings.
smt2 :package: - SMT-LIB 2 parsing library.
tptp :package::star::zzz: - parse the TPTP format.
Yaspar :package: - a parser for the SMT-LIB 2.7 language generated by the LARLPOP parser generator.

Bindings

bddminisat-sys :package: - FFI bindings to bdd_minisat_all, a BDD-based AllSAT solver.
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-rs :package: - bindings for the CaDiCaL SAT solver.
cadical-sys :package: - almost complete safe and unsafe bindings for the CaDiCal SAT solver.
cat_solver :package: - bindings for the Kissat SAT solver.
clingo-rs :package::package::package::star: - idiomatic bindings to the clingo library.
cplex-rs :package::package: - safe rust bindings for CPLEX.
cryptominisat-rs :package::zzz: - bindings for CryptoMiniSat.
cvc5-rs :package::package: - safe, high-level Rust bindings for the cvc5 SMT solver.
EasyZ3 :package: - simplified API to get started with the z3 SAT solver.
Espresso Logic Minimizer :package::package: - bindings to the Espresso heuristic logic minimiser from UC Berkeley.
falcon-z3 :package: - bindings for Z3.
highs :package: - safe rust bindings for the HiGHS linear programming solver.
highs-sys :package: - bindings for the HiGHS linear programming solver.
IPASIR :package::zzz: - FFI bindings for the IPASIR incremental SAT solver interface.
Ipasir-loading :package: - load shared libraries of IPASIR compatible SAT solvers.
isabelle-client :package: - client to interact with an Isabelle server.
Kissat-rs :package: - bindings for the Kissat SAT solver.
lean-sys :package::star: - bindings to Lean 4's C API.
Leo3 :package::package::package::package: - safe, ergonomic Rust bindings to the Lean4 theorem prover, inspired by PyO3's architecture.
libsmt.rs :zzz: - bindings for SMTLIB2.
logicng-open-wbo-sys :package: - low-level LogicNG bindings for the MaxSAT solver Open-WBO.
lpsolve :package::package::zzz: - high-level lpsolve wrapper.
maxpre-rs :package: - bindings for the (multi-objective) MaxSAT preprocessor MaxPre.
pblib-rs :package: - safe bindings for pblib.
rplex :zzz: - bindings for CPLEX.
rsmaxsat :package: - bindings for EvalMaxSAT .
rsmt2 :package::package::star::zzz: - generic library to interact with SMT-LIB 2 compliant solvers.
rssat :package::skull: - bindings for multiple popular SAT solvers, superseded by satgalaxy-rs.
russcip :package::star: - safe Rust interface for SCIP.
Rust-SMT-LIB-API :package::star::skull: - generic high-level API for interacting with SMT solvers.
rust_z3prover :zzz: - use Z3 SMT solver from rust.
rustproof-libsmt :package::zzz: - fork of libsmt.rs.
SAT Nexus - interfaces and wrappers for SAT solvers.
satgalaxy-rs :package: - FFI bindings for satgalaxy-core bringing high-performance SAT solving to Rust.
scip-sys :package: - raw rust bindings to SCIP.
smt_sb-rs :package: - Z3 SMT Simple Binding.
smtlib :package::package::package: - high-level API for interacting with SMT solvers.
vampire-rs :package::package: - safe Rust bindings to the Vampire theorem prover for first-order logic with equality.
vipers - crates for interacting with the Viper verification infrastructure.
Yices2 :package::package: - low and high-level bindings to the Yices2 SMT solver.
z3 :package::package::star::fire: - high-level and low-level Rust bindings for the Z3 solver.
z3-rust :package: :zzz: - high level bindings for the Microsoft's Z3 SMT solver.
Z3D :package::zzz: - Z3 DSL interface.

Translator

anthem :package::fire: - translate answer set programs to first-order theorem prover language (v2, complete rewrite).
bool2dimacs :package: - transfer boolean expression to dimacs directly.
CNFGEN :package: - create boolean formulae from boolean expressions and integer expressions.
CNFGEN 2 :package: - newer version of CNFGEN - DIMACS CNF generator.
Cnfpack :package: - converts between DIMACS CNF file format and the compressed binary Cnfpack format.
Decdnnf-rs :package: - translating formulas generated by d4 into the format generated by c2d.
hz-to-mm0 :zzz: - translator from HOL Zero / Common HOL to Metamath Zero.
Metamath hammer - tool for automatically proving Metamath theorems using ATPs.
pindakaas :package::package::package::package::package::package: - transform integer and pseudo Boolean constraints into conjunctive normal form.
rust-smt-ir :package::package::star: - intermediate representation (IR) in Rust for SMT-LIB queries.

Misc

AbsoluteUnity :zzz: - think Prolog, but less capable.
Alice_rs :lab_coat::lab_coat::zzz: - implementation of a decision procedure for A Decidable Fragment of Separation Logic.
auto :lab_coat: - decision procedure for intuitionistic logic.
Avatar Hypergraph Rewriting :package::zzz: - hypergraph rewriting system with avatars for symbolic distinction.
coc :zzz: - the calculus of constructions.
compiler :package::baby_chick::zzz: - trivial compiler framework for Metamath Zero binary proofs.
discrimination-tree :package: - discrimination tree term indexing.
easy-smt :package::star: - easy SMT solver interaction (Inspired by the simple-smt haskell package.).
egg :package::star: - flexible, high-performance e-graph library.
epilog :package::zzz: - collection of Prolog-like tools for inference logic.
FALL :package::zzz: - easily embeddable, futures-friendly logic engine.
foliage :package::zzz: - first-order logic with integer arithmetics.
fuzzylogic :package: - provides operations and inference for fuzzy set theory.
Joker Calculus :package: - implementation of Joker Calculus in Rust.
Kravanenn :star::zzz: - set of tools for Coq.
logic-lang :package: - structural logic based on equivalence graphs.
logical_solver :package::baby_chick: - library for solving and parsing logical equations.
Logician :package: - type-safe SMT solver driver.
LogicNG :package: - library for creating, manipulating and solving Boolean and Pseudo-Boolean formulas.
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 :zzz: - utility tools for Metamath Zero binary proof files.
mmb-types :package::zzz: - library containing the definitions of the opcodes in the Metamath Zero binary proof files.
moniker :package::package::star::zzz: - automagical variable binding library.
nanoda :star::skull: - became nanoda-lib.
nanoda_lib :star: - type inference/checking functionality based on the Lean theorem prover.
nnf :package: - Negation Normal Form manipulation library.
polytype :package::star: - Hindley-Milner polymorphic typing system.
program-induction :package::star: - library for program induction and learning representations.
ruler :diamonds::star::lab_coat: - rewrite rule inference using equality saturation.
Rust First Order Logic :package: - syntax of First Order Logic with self-consistent logical assertions.
rust-nbe-for-mltt :star: - normalization by evaluation for Martin-Löf Type Theory with dependent records.
rust-smt-strings :package: - library for strings as defined in the SMT-LIB theory of strings.
~~rust-unify~~ :package: :recycle::lab_coat: - unification algorithum implementation.
RustSAT :package::package::package::package::package::package::package::package::package::star: - provide elements commonly used in satisfiability solving software.
Rusty Razor :package::package::package::star::zzz: - tool for constructing finite models for first-order theories.
sat-interface :package: - abstraction interface for SAT solvers.
sat-solvers :package: - unified Rust interface to multiple SAT solvers with automatic source compilation.
sat_toasty_helper :package: - convenient way to write and solve SAT constraints.
Satoxid :package: - library to help with encoding SAT problems.
smt2utils :package::package::package::package::skull: - libraries and tools for the SMT-LIB-2 standard.
smtlib-syntax :package: - syntactic types the for the SMT-LIB 2.6 spec. Meant for code generation, not parsing.
term-rewriting-rs :package::star::zzz: - representing, parsing, and computing with first-order term rewriting systems.
tribool :package::zzz: - three-valued logic.
The Trivial Metamath Zero kernel :package::zzz: - Metamath Zero kernel for Trivial.
Whisper :star::zzz: - logic Programming DSL.
xmt-lib :package: - grounder for SMT solvers.
Yaspar-IR :package: - provides a few representations of SMT scripts and other functionalities.

Books code

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

harrison-rust :book::star: - library for SAT solving and automated theorem proving derived from the book.
logic-rs :book::star::zzz: - parser of relational predicate logic & truth tree solver
plar-rs :book::zzz::ghost: - exploring John Harrison's Handbook of Practical Logic and Automated Reasoning.
program-proofs-prusti :book: - examples and exercises from the book Program Proofs by K. Rustan M. Leino.
tapl :zzz: - implementation of TAPL.
TAPL Implementations - collection of implementations of TAPL (Chap 3-7,9,11,13-14,19,22).
TAPL in Rust :star::zzz: - collection of implementations of TAPL (Chap 3-10,17,25).
The Little Prover :book: - transpiled J-Bob assistant & GUI frontend.
the-little-typer :book: - a Rust take on D.Friedman's book.
tnt :book::package: - implementation of Hofstader's "Typographical Number Theory" from the book Gödel, Escher & Bach.
types-and-programming-languages :star::zzz: - Exercises from TAPL textbook + extras! (Chap 5-7,9-10)

Programming Language

beta - dependently-typed programming language, aiming to support a cubical interpretation of univalence.
egglog :package::star::lab_coat: - language that combines the benefits of equality saturation and datalog.
Fathom :package::star::construction: - declarative data definition language for formally specifying binary data formats.
High-order Virtual Machine (HVM) :star: - massively parallel, optimal functional runtime.
Interaction Calculus :package::star: - programming language (fit the optimal λ-calculus reduction algorithm perfectly).
isotope-prover-experiments :lab_coat::lab_coat::skull: - experimental dependently typed language supporting borrow checking.
Kind :package::star: - next-gen functional language and proof assistant.
Last Order Logic :package: - experimental logical language.
Lean-Claude - rewrite Lean4 Compiler in Rust, using only Claude Code.
Logicaffeine :package::package::package::package::package::package::package::package::package::package::package::star: - compiles your words into programs, proofs, and formal systems.
minihl - formal methods playgorund for MiniHeapLang language.
minitt-rs :package::package::star::skull: - became Voile.
Narc :package::star::zzz: - dependently-typed programming language with Agda style dependent pattern matching.
norem-lang - pure functional programming language with automatic verification and effect system.
Pika :star::construction: - small, performance-oriented, dependently typed ML with algebraic effects and unboxed types..
Pikelet :package::star::zzz: - small, functional, dependently typed programming language.
proto-vulcan :package::package: - miniKanren-family relational logic programming language.
reckon :star: - programming language designed for reasoning tasks, proof checking, and logical inferencing.
rooc :mortar_board::star: - a language for compiling formal mathematical models into static models.
Rust pi-forall :lab_coat: - partial re-implementation of pi-forall.
Scryer Prolog :package::star: - modern Prolog implementation.
SMT-language :package: - Sat Modulo Theory Language.
stupid-see :baby_chick::zzz: - symbolic execution engine. Mainly targeted at the verification course in THU.
tako - experimental programming language for ergonomic software verification.
TIP :baby_chick::zzz: - programming language aimed at teaching fundamental concepts of static program analysis.
Untyped Concatenative Calculus :zzz: - toy programming language and prototype for Dawn.
Untyped Multistack Concatenative Calculus - toy programming language and prototype for Dawn.
Voile :package::package::star::zzz: - became Narc.
zz :package::star::skull: - 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::zzz: - miniKANREN as a DSL.
rslogic :package::star::zzz: - logic programming framework for Rust inspired by µKanren.
rust-kanren :star::zzz: - loose interpretation of miniKanren and cKanren.
µKanren-rs :package::star: - implementation of µKanren.

Lambda Calculus

blc :package::zzz: - implementation of the binary lambda calculus.
Closure Calculus :package::lab_coat::zzz: - library for Barry Jay's Closure Calculus.
lam - lambda calculus evaluator.
Lamb :package::mortar_board: - implementation of the pure untyped lambda calculus in modern, safe Rust.
lambash :package::zzz: - λ-calculus shell.
~~lambda_calc~~ :package::recycle: - command-line untyped lambda calculus interpreter.
lambda_calculus :package::star: - simple, zero-dependency implementation of pure lambda calculus in safe Rust.
lambda_calculus :zzz: - lambda calculus with antlr grammar.
lambdacube :construction::zzz: - implementation of the lambda cube (and other type stuff).
Lambda Shell :package: - simple REPL shell for untyped lambda expressions.
Lambdascript - educational tool illustrating beta reduction of untyped lamba terms.
Lamcal :package::package::zzz: - lambda calculus parser and evaluator and a separate command line REPL.
lalrpop-lambda :package::star: - λ-calculus grammar/interpretor written using LALRPOP and λ!.
Pun Calculus :package: - variant of Typed Lambda Calculus with generalized variable punning (ad-hoc polymorphism).
RLCI :star: - Overly-documented Lambda Calculus Interpreter.
type-theory :star: - typed λ-calculus.

Propositional logic

~~Chevre~~ :recycle: - small propositional logic interpreter.
clawgic :package: - logic engine for making, modifying, and evaluating expressions from sentential logic.
hooo :package: - propositional logic with exponentials (HOOO EP).
implies :package: - storing logical formulas as parse trees and performing complex operations on them.
logic :package::baby_chick::zzz: - crate for propositional logic.
logic-resolver :baby_chick::zzz: - toy implementation of resolution for propositional logic.
Logic Tracer :package::package::package: - reads a logical proposition and interprets it to build the truth table and the AST.
mini-prop :package: - CLI tool for parsing and processing LaTex formatted propositional statements.
plc :zzz: - propositional logic calculator.
Plogic :star: - propositional logic evaluator and rule-based pattern matcher.
Prop :package::star: - library for theorem proving with Intuitionistic Propositional Logic.
Propositional Logic :package::mortar_board: - propositional Logic Library.
Propositional logic evaluator :package: - propositional logic evaluator (truth tables for propositional expressions).
Propositional Tableaux Solver :package::zzz: - solver using the propositional tableaux method.
prop_tune :package::package::package: - library for working with Logical Propositions.
raa_tt :package: - prover for sentences of propositional calculus.
Resolution Prover :zzz: - resolution prover library for propositional logic.
resolution-prover :zzz: - Uses propositional resolution to prove statements and proofs on discord.
rs-logik :ghost: - propositional logic interpreter.
rust-proplogic-toylang :baby_chick: - toy language for Propositional Logic.
rusty-logic :baby_chick::zzz: - propositional logic analysis.
simple-proof-assistant :baby_chick::zzz: - a proof assistant kernel for minimal propositional logic.
type-proof :package::package: - crate for type-checked propositional logic proofs.
validator :zzz: - small utility to test a propositional logic theorem prover.

Unclassified

Croissant - crossword solver backed by various SAT solvers.
formal-systems-learning-rs :zzz: - simulations to learn formal systems as typed first-order term rewriting systems.
Hashi - Bridges Puzzle - Hashi Puzzle (aka Bridges) solver.
inf402 - SAT-solver-based takuzu solver.
Junglefowl :package::package: - runs Peano arithmetic on Rust types, verified at compile time..
list-routine-learning-rs :zzz: - to learn typed first-order term rewriting systems that perform list routines.
logical_tui :baby_chick: - tui for logical_solver.
Minimal models :zzz: - uses a SAT solver to find minimal partial assignments that are model of a CNF formula.
n-queens-sat :zzz: - modelling n-queens problem as conjunctive normal form and solving it with DPLL algorithm.
nonogrid :package: - lightning fast nonogram solver.
Relog - implementation of several strongly-normalizing string rewriting systems.
roq :package::package: - proc-macro Coq code generation and proof automation.
rummy_to_sat - implementation of a solver for Rummy.
rust-z3-practice :zzz: - solving a number of SAT problems using Z3.
Satisfaction :lab_coat: - investigate phase transitions in k-SAT problems.
sudoku_sat - solve Sudoku variants with SAT solvers.
Supermux :zzz: - reduction of the superpermutation problem to Quantified Boolean Formula.
Supersat :zzz: - attempt to find superpermutations by reducing the problem to SAT.
tarpit-rs :star::zzz: - type-level implementation of Smallfuck. Turing-completeness proof for Rust's type system.
Type System Chess :star: - chess implemented entirely in the Rust type system.
VeriFactory :star: - verifier for Factorio blueprints.

Resources

Books

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

Research Paper & Thesis

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.
rust-smt-ir-examples - examples of using a rust-smt-ir, a Rust intermediate representation (IR) for SMT-LIB.
aws-lambda-z3 - tutorial on running Z3 on AWS Lambda, with Rust.

Blogs

A Formal Verification of Rust's Binary Search Implementation. :uk:
Formal Land :uk:
Kani Rust Verifier Blog :uk:
Mist 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::diamonds:

Posts

Visions of the future: formal verification in Rust - 2024
Some notes on Rust, mutable aliasing and formal verification :diamonds: - 2024
Cracking the Cryptic (with Z3 and Rust) - 2024
How Open Source Projects are Using Kani to Write Better Software in Rust - 2023.
Check AI-Generated Code Perfectly and Automatically - 2023.
Solving The Witness with Z3 - 2022.
Formally Verifying Rust's Opaque Types - 2022.
An adventure with optimization, Rust and Z3 - 2019.

Crates keywords

verification - 271 entries. :100:
solver - 213 entries. :100:
logic - 186 entries. :100:
smt - 77 entries. :100:
sat - 65 entries. :100:
satisfiability - 41 entries. :100:
linear-programming - 33 entries. :100:
lean - 32 entries. :100:
dependent-types - 18 entries. :100:
proving - 16 entries. :100:
proof-assistant - 15 entries. :100:
prover - 13 entries. :100
z3 - 13 entries. :100:
smt-lib - 12 entries. :100:
cnf - 12 entries. :100::
sat-solver - 10 entries. :100:
rewriting - 10 entries. :100:
dimacs - 9 entries. :100:
first-order - 6 entries. :100:
metamath-zero - 5 entries. :100:

Community

Mikko Aarnos - Serkr.
Johannes Altmanninger - rate.
ammkrn - ~~nanoda~~, nanoda_lib, second_opinion.
AndPuQing - Leo3.
Bruno Andreotti - Carcara.
Arata - lutrix.
arbaregni - resolution-prover.
astrobeastie - sequentprover.
Alexis Aurandt - r2u2_core.
Yechan Bae - Rudra, Satire.
Clark Barrett - ~~Rust-SMT-LIB-API~~.
Mathieu Baudet - ~~smt2utils~~.
Mike Beaumont - rust-sat.
Antoine Belvire - Croissant.
Tim Beurskens - RsBDD.
Matteo Biggio - cplex-rs.
Aurel Bílý - program-proofs-prusti.
Justin Blanchard - cat_solver.
boitsov14 - theorem-prover-rs.
James Bornholt - rustsat(2), Shuttle.
Henrik Böving - Obvious.
Oliver Bøving - Mist, smtlib, vipers.
Lee ByeongJun - Lambda Calculus Parser.
Bickio O'Callahan - Solving The Witness with Z3.
Pierre Carbonnelle - m2cSMT, xmt-lib.
Mario Carneiro - coq-rs, FRAT-rs, hz-to-mm0, isabelle export tool, Metamath hammer, Metamath-knife, Mizar proof checker, mm0-rs, olean-rs.
Tej Chajed - Temporal Verifier.
Adrien Champion - hoice, ~~Kinō~~, matla, Mikino, rsmt2, SAT-MICRO, Verification for Dummies.
David Chanin - Tensor Theorem Prover.
Michelle Cheatham - rusty-logic.
Thomas Chaumeny - Satisfaction.
Jimmy Chen Chen - theorem-prover.
Alex Chew - Z3D.
Konstantin Chukharev - SAT Nexus, backdoor-solver.
Guillaume Claret - coq-of-rust, Formal Land.
Cobalt - SAT solver ANalyser.
CoCoSol - logiq.
Lorenzo Colombini - Colombini-SAT.
convexbrain - Totsu.
David Cox - mps.
Simon Cruanes - BatSat.
Dacit - Sequent solver.
dandxy89 - lp_parser_rs.
Azeez Daoud - ceetle.
DavidD12 - SMT-language, smt_sb-rs.
Ariel Davis - coc.
Liam Davis - StalmarckSAT.
Jip J. Dekker - pindakaas.
Xavier Denis - Creusot, RustHornBelt: A Semantic Foundation for Functional Verification of Rust Programs with Unsafe Code, RustHornBelt Library & Benchmarks, Rust verification tools (2021), Specifying and Verifying Higher-order Rust Iterators (2023), A hybrid approach to semi-automated Rust verification (2024), Visions of the future: formal verification in Rust.
Sushant Dinesh - libsmt.rs.
Sylvie Dirkswager - Pika.
Craig Disselkoen - boolector.
Andrei Dobrescu, Marian Călborean - INCL Automated Theorem Prover.
Dragon-Hatcher - Type System Chess, vampire-rs, watson.
Mark Drobnak - p4-analyzer.
Bruno Dutertre - rust-smt-ir, rust-smt-ir-examples, rust-smt-strings.
Thomas Dziedzic - lambda_calculus.
Kurt Ehlert - ellp.
Trevor Elliott - auto, easy-smt.
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.
Nathan Fenner - sat_toasty_helper.
Jonáš Fiala - SMTSCOPE.
FireFighterDuck - Alice_rs, Kissat-rs, minihl.
Paolo Flores - logic-parser.
Hugo Frezat - logic-lang.
Robin Freyler - CNF Parser, DIMACS Parser, Stevia.
Lennard Gäher - RefinedRust.
Galois, Inc. - crux-mir.
Alexey Gerasimov - Liquid Rust.
Jad Ghalayini - ~~isotope-prover-experiments~~, lean-sys.
Mohammed Ghannam - russcip, scip-sys.
Nicola Gigante - ::formally.
Nathan Graule - rs-logik.
Brandon H. Gomes - qbar.
Vinicius Gomes - NanoSAT, ~~satsol~~.
William Goodall - roq.
Robert Grosse - cryptominisat-rs.
Alexandru Jercan - Croof.
Travis Hance - verified-memory-allocator.
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, Verification of a Rust Implementation of Knuth's Dancing Links using ACL2.
Tristen Harr - Logicaffeine.
Rowan Hart - Yices2.
Timothée Haudebourg - smt2.
Reuben Hillyard - beta.
Son HO - Charon.
Sarek Høverstad Skotåm - CreuSAT.
Hoblovski - stupid-see, stupid-smt.
Graydon Hoare - Some notes on Rust, mutable aliasing and formal verification.
Emil Hofstetter - mini-prop, prop_tune.
Khaled Hosseini - Propositional logic evaluator.
hrkzmnm - rust_z3prover.
Jason Hu - cvc5-rs, sat-interface, Yaspar, Yaspar-IR.
Tero Huttunen - proto-vulcan.
Noel Huibers - Hashi - Bridges Puzzle.
ibrahimcesar - lolli.
Christoph Jabs - Scuttle, maxpre-rs, rustsat.
Bart Jacobs - VeriFast.
Alex Jackson - sat-solvers.
Jan - Plogic.
Paweł Jastrzebski - Propositional Logic.
Ranjit Jhala - flux-demo.
Andrew Johnson - LSTS, Pun Calculus, Relog.
Evan Johnson - VeriWasm.
Dylan R. Johnston - Formally Verifying Rust's Opaque Types.
Matthias Jugan - LogicNG, logicng-open-wbo-sys.
Ralf Jung - Understanding and Evolving the Rust Programming Language, Miri: Practical Undefined Behavior Detection for Rust.
Oskari Jyrkinen - Axiom Profiler 2.0.
jzbor - Lambda Shell.
Carl Kadie - Check AI-Generated Code Perfectly and Automatically.
Hosein Kalbasi - akim.
Igor Kalichevski - nnf.
karroffel - contracts.
Anto Keinänen - logical_solver, logical_tui.
Franziskus Kiefer - Hax.
Tetsuya Kitahata - Legalis-RS, OxiLean, OxiZ.
Mike Kuykendall - Logician.
Rahul Kumar - How Open Source Projects are Using Kani to Write Better Software in Rust, Rust std-lib verification.
Prateek Kumar - ~~msat~~, ~~rsat~~, ~~slp~~, ~~SolHOP~~.
Alexey Kutepov - Noq.
Kevin Lacker - Acorn.
Ivan Ladelshchikov - nonogrid.
Kevin Laeufer - Patronus.
Aleksandr Larionov - bootfrost.
Andrea Lattuada - verus.
lcnr - ~~cobalt~~.
Shea Leffler - tarpit-rs, whisper.
Alessandro Legnani - VeriFactory.
Nico Lehmann - Flux.
Carl Lerche - Loom.
Chuck Liang - Lambdascript.
Nathan Lilienthal - lambash, lalrpop-lambda.
ljedrz - blc, lambda_calculus.
Ophir LOJKINE - highs, highs-sys, good_lp.
Emmanuel Lonca - Decdnnf-rs, Ipasir-loading, pblib-rs, scalop.
Kevin Lotz - isabelle-client, smt-str.
Andrew Luka - cadical-sys.
Patrick Lühne - anthem, foliage.
Michael Madden - Xori.
Scott J Maddox - Untyped Concatenative Calculus, Untyped Multistack Concatenative Calculus.
Indraneel Mahendrakumar - Lamb.
Harald Maida - Lamcal.
Krzysztof Małysa - ~~prover~~.
Manas - fuzzylogic.
MarcoTz - TAPL Implementations.
Miklos Maroti - cadical-rs, relsat-rs, uasat-rs.
marshtompsxd - verifiable-controllers.
Niko Matsakis - Chalk, Kani, plar-rs.
Yusuke Matsushita - Extensible Functional-Correctness Verification of Rust Programs by the Technique of Prophecy, RustHorn.
mbillingr - miniKANREN, The Little Prover, the-little-typer.
adam mcdaniel - reckon.
mcmfb - ~~lambda_calc~~.
Tom Meyer - Granite.
Alexander Mishunin - minisat-rust.
Proloy Mishra - lam, nnoq, nyaya.
Bruce Mitchener - z3.
Lucas Morales - polytype, program-induction.
Jesse Mu - satyrs.
Dominic Mulligan - Supervisionary.
Jon Nadal - Stateright.
Chandrakana Nandi - Ruler.
neuring - rummy_to_sat, Satoxid.
Sven Nilsen - Avalog, Avatar Hypergraph Rewriting, Caso, Debug-SAT, hooo, Joker Calculus, Last Order Logic, linear_solver, Monotonic-Solver, pocket_prover, pocket_prover-set, Poi, Prop, reachability_solver.
Yuichi Nishiwaki - shari.
Chase Norman - Canonical.
Stefan O'Rear - smetamath.
Robert Obkircher - sat-solver.
Adolfo Ochagavía - An adventure with optimization, Rust and Z3.
Jan Onderka - Machine-check.
Edgar Onghena - inf402.
Alex Ozdemir - rlfsc.
Mohsen Pakzad - Rustplex.
PatrickTheElder - EasyZ3.
Chris Patuzzo - Supermux, Supersat.
Pierre-Marie Pédrot - Kravanenn.
Hugo Peters - Cracking the Cryptic (with Z3 and Rust).
Arvid E. Picciani - zz.
Anton Ping - norem-lang.
Dan Pittman - Bounded Registers.
Gabriel Poesia - minimo.
Nadia Polikarpova - cyclegg.
Christian Poveda - ~~Chevre~~.
Bobby Powers - Logically Qualified Data Types.
Joshua Pratt - ArcsJs - Provable, tako.
petersn - autosat.
Boqin Qin - lockbud.
Armaan Rashid - implies.
Michael Rawson - discrimination-tree, lazyCoP, ~~lerna~~, lickety, HopCoP, SATCoP, tptp.
Alastair Reid - Articles about a collection of tools/libraries to support both static and dynamic verification of Rust programs, Rust Software Verification Benchmarks, Rust verification tools, Rust verification tools list.
Adrien Renaudineau - sat_lab.
Fernando Bryan Reza Campos - Logic Tracer.
Corey Richardson - lpsolve.
Nathan Ringo - FALL.
Benjamin Rogers-Newsome - Rust First Order Logic.
Erik Rohkohl - n-queens-sat.
Olivier ROLAND - mrs, mrs-tptp.
Marco Concetto Rudilosso - validator.
Josh Rule - formal-systems-learning-rs, list-routine-learning-rs, term-rewriting-rs.
Salman Saghafi - rust-z3-practice, Rusty Razor.
Michael Salter - Rustproof, rustproof-libsmt.
Marcos Sartori - Espresso Logic Minimizer.
Robert Scheidegger - microsat.
Daniel Schemmel - DRSAT.
Ryan Schroeder - AbsoluteUnity, epilog.
Carol Schulze - gpp-solver.
Klas Segeljakt - type-theory.
shinkwhek - SAT solver.
skbaek - t3p.
Narazaki Shuji - SAT-bench, Splr, Splr notebook, sudoku_sat.
Konstantin Sidorov - How to discover short, shorter, and the shortest proofs of unsatisfiability, simple-stat.
Jörg Singer - raa_tt.
J David Smith - rplex.
SnO₂WMaN - rust-proplogic-toylang.
snsinfu - dpll-sat.
Takehide Soh - bddminisat-sys.
Mikhail Solovev - bitwuzla-sys, boolector-sys.
Ben Sparkes - otter_sat.
Specy - microlp, rooc.
Dennis Sprokholt - aws-lambda-z3, Rust pi-forall.
Will Sturgeon - Junglefowl.
Yuheng Su - logic-form, rIC3 Hardware Model Checker.
SymmetricChaos - tnt.
Mateusz Szpakowski - CNFGEN, CNFGEN 2, Exec-SAT.
Lucas Tabary-Maujean - Proost.
Victor Taelin - High-order Virtual Machine (HVM), Kind2, Interaction Calculus.
Calin Tataru - homotopy-rs.
Sven Thiele - clingo-rs.
Mark Thom - Scryer Prolog.
Fabian Thorand - LogRu.
Arthur Tilley - harrison-rust.
Hitoshi Togasaki - scrapsat, screwsat.
Callum Tolley - plc.
William Towler - type-proof.
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).
Noel vanSchaick - clawgic.
Pavol Vargovčík - z3-rust.
Herman Venter - MIRAI, Rust static analysis/verification reading and resources.
Mark Verleg - prover(2).
Nathaniel Victor - SAT Solver(2).
Nikita Voronov - RLCI.
Xinyi Wan - vostd.
John Wang - rust-metamath.
Shuxian Wang - QED Prover.
Max Willsey - egg, egglog.
Ivo Wingelaar - compiler, mmb-binutils, mmb-parser, mmb-types, The Trivial Metamath Zero kernel, Verifier.
Jan Winkelmann - smtlib-syntax.
wvhulle - lean-tui.
Florian Würmseer - SAT-Solver.
Jieyou Xu - Propositional Tableaux Solver.
Chenyuan Yang - AutoVerus: Verus Proof Synthesis.
Ren Yanjie - bool2dimacs, RustLogic.
Yi Cai - vest.
Brendan Zabarauskas - Fathom, moniker, Pikelet, rust-nbe-for-mltt.
Bas Zalmstra - Resolvo.
Alexey Zatelepin - ~~minilp~~.
Xiyu Zhai - Lean-Claude.
Eric Zhang - µKanren-rs.
Hanliang Zhang - sat.
Tesla Ice Zhang - ~~minitt-rs~~, Narc, Voile.
Lin Zhengyao - verdict.
Xie Zhongtao - rsmaxsat, ~~rssat~~, satgalaxy-rs.
Felix Zhu - lambdacube.
Li Zhuohua - MirChecker.
Philip Zucker - res-rs.

Awesome rust formalized reasoning

About

Contents

Legend