The trust-minimized, zero-knowledge bridging protocol, designed for censorship resistance, extremely high security, and usage in decentralized finance.
An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.
An automatic theorem prover in OCaml for typed higher-order logic with equality and datatypes, based on superposition+rewriting; and Logtk, a supporting library for manipulating terms, formulas, clauses, etc.
Cicada Language (solo version)
Zero-Knowledge Proofs "for (not too much 😉 ) dummies"
Resolution theorem proving for predicate logic in pure Python.
Cicada Language (PLCT little team)
A community-developed re-implementation of the Starkware Stone Prover
Python Symbolic Information Theoretic Inequality Prover
[research] A modular SMT solver in OCaml, based on mcSAT
A modular library for CDCL(T) SMT solvers, with [wip] proof generation.
A HOL-based framework for reasoning over knowledge graphs
Python library for computational formal logic, formal semantics, and theorem proving
Nexus is ZkVM a Modular Verifiable Internet. A Complete Guide - Run Nexus node as Prover Network.
Haskell interface to automated theorem provers
An awesome list of prover mechanism resources of the zk ecosystem
Add a description, image, and links to the prover topic page so that developers can more easily learn about it.
To associate your repository with the prover topic, visit your repo's landing page and select "manage topics."