unionlabs/union

The trust-minimized, zero-knowledge bridging protocol, designed for censorship resistance, extremely high security, and usage in decentralized finance.

Language: Rust - Size: 442 MB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 54,480 - Forks: 2,723

newca12/awesome-rust-formalized-reasoning

An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.

Size: 312 KB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 330 - Forks: 11

eprover/eprover

Language: C - Size: 147 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 138 - Forks: 25

niluferokay/awesome-prover-mechanisms

An awesome list of prover mechanism resources of the zk ecosystem

Size: 14.6 KB - Last synced at: 10 days ago - Pushed at: 10 days ago - Stars: 7 - Forks: 1

ozekik/mathesis

Python library for computational formal logic, formal semantics, and theorem proving

Language: Python - Size: 1.18 MB - Last synced at: 3 days ago - Pushed at: about 2 months ago - Stars: 21 - Forks: 3

sneeuwballen/zipperposition

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.

Language: OCaml - Size: 29.3 MB - Last synced at: 1 day ago - Pushed at: 6 months ago - Stars: 141 - Forks: 17

evhub/pyprover

Resolution theorem proving for predicate logic in pure Python.

Language: Python - Size: 344 KB - Last synced at: 21 days ago - Pushed at: over 1 year ago - Stars: 93 - Forks: 10

arcxteam/nexus-node

Nexus is ZkVM a Modular Verifiable Internet. A Complete Guide - Run Nexus node as Prover Network.

Language: Shell - Size: 90.8 KB - Last synced at: 2 days ago - Pushed at: about 2 months ago - Stars: 8 - Forks: 2

SKaaalper/Nexus-CLI

Size: 53.7 KB - Last synced at: about 1 month ago - Pushed at: about 2 months ago - Stars: 7 - Forks: 3

zunxbt/nexus-prover

One click guide to run nexus prover beta on your system

Language: Shell - Size: 30.3 KB - Last synced at: 6 days ago - Pushed at: about 2 months ago - Stars: 1 - Forks: 0

RaphaelBonatti/propositional-logic-prover-python

A propositional logic prover implemented using resolution refutation.

Language: Python - Size: 43 KB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 0 - Forks: 0

aztek/atp

Haskell interface to automated theorem provers

Language: Haskell - Size: 352 KB - Last synced at: 6 days ago - Pushed at: about 3 years ago - Stars: 9 - Forks: 0

SDZZGNDRC/ToyProver

A toy-level automated theorem prover written in Lean4, aimed at learning Lean4 and automated theorem proving

Language: OpenEdge ABL - Size: 1000 Bytes - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 0 - Forks: 0

c-cube/sidekick

A modular library for CDCL(T) SMT solvers, with [wip] proof generation.

Language: SMT - Size: 15.4 MB - Last synced at: 1 day ago - Pushed at: 3 months ago - Stars: 24 - Forks: 15

cheuktingli/psitip

Python Symbolic Information Theoretic Inequality Prover

Language: Python - Size: 2.56 MB - Last synced at: 24 days ago - Pushed at: about 1 year ago - Stars: 37 - Forks: 8

dipdup-io/stone-packaging

Various forms of distribution for the Starkware Stone prover and verifier

Language: Shell - Size: 5.66 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 17 - Forks: 29

thor314/pebble-stark

A community-developed re-implementation of the Starkware Stone Prover

Language: Rust - Size: 321 KB - Last synced at: 19 days ago - Pushed at: 6 months ago - Stars: 69 - Forks: 6

cicada-lang/cicada-plct

Cicada Language (PLCT little team)

Language: TypeScript - Size: 2.51 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 92 - Forks: 7

cicada-lang/cicada-solo

Cicada Language (solo version)

Language: TypeScript - Size: 6.83 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 128 - Forks: 5

baro77/ZKbasicsCS

Zero-Knowledge Proofs "for (not too much :wink: ) dummies"

Size: 854 KB - Last synced at: 5 months ago - Pushed at: over 1 year ago - Stars: 119 - Forks: 7

IBM/ULKB

A HOL-based framework for reasoning over knowledge graphs

Language: Jupyter Notebook - Size: 13.9 MB - Last synced at: 4 months ago - Pushed at: 6 months ago - Stars: 24 - Forks: 4

xieyuheng/skolem

an ACL2 style theorem prover with structural diff, embedded in scheme.

Language: Scheme - Size: 56.6 KB - Last synced at: 4 months ago - Pushed at: about 6 years ago - Stars: 2 - Forks: 0

sazare/cheaplogic

analyzer of the proof structure of a clause set by resolution and HOW TO WRITE THE WORLDS BY FOL.

Language: Common Lisp - Size: 19.4 MB - Last synced at: 2 months ago - Pushed at: 8 months ago - Stars: 1 - Forks: 0

iosis-tech/zetina

Shared peer-to-peer network of zero-knowledge provers

Language: Cairo - Size: 1.08 MB - Last synced at: 11 months ago - Pushed at: 11 months ago - Stars: 8 - Forks: 1

c-cube/mc2

[research] A modular SMT solver in OCaml, based on mcSAT

Language: SMT - Size: 9.08 MB - Last synced at: 1 day ago - Pushed at: over 1 year ago - Stars: 39 - Forks: 5

rohitanwar/Ostara

A simple automated theorem prover written in Haskell

Language: Haskell - Size: 331 KB - Last synced at: 12 months ago - Pushed at: 12 months ago - Stars: 0 - Forks: 0

geometer/sandbox

Geometer's Sandbox project repo

Language: Python - Size: 2.23 MB - Last synced at: 16 days ago - Pushed at: about 1 year ago - Stars: 6 - Forks: 0

rikosellic/ZFC-prover-in-Coq

A mini ZFC prover embedded in Coq for teaching scenarios. (CoqPL'23)

Language: Coq - Size: 107 KB - Last synced at: over 1 year ago - Pushed at: about 2 years ago - Stars: 1 - Forks: 1

kaicho8636/pyprover

Python-based theorem prover

Language: Python - Size: 6.52 MB - Last synced at: over 1 year ago - Pushed at: about 2 years ago - Stars: 3 - Forks: 0

9Y0/NaturalDeduction

A natural deduction prover in Gentzen's system.

Language: Haskell - Size: 25.4 KB - Last synced at: over 1 year ago - Pushed at: over 3 years ago - Stars: 0 - Forks: 0

ExcaliburZero/resolution-prover

An implementation of a propositional logic resolution prover in Rust.

Language: Rust - Size: 900 KB - Last synced at: 11 months ago - Pushed at: over 6 years ago - Stars: 4 - Forks: 0

moratori/clover

A experimental prover written in Common Lisp, based on clause resolution and Knuth-Bendix completion algorithm.

Language: Common Lisp - Size: 443 KB - Last synced at: almost 2 years ago - Pushed at: almost 3 years ago - Stars: 1 - Forks: 0

c-cube/frog-utils 📦

[frozen] Scheduling and running jobs on a shared computer, then analyse their output

Language: OCaml - Size: 714 KB - Last synced at: 1 day ago - Pushed at: over 6 years ago - Stars: 5 - Forks: 0

SauzeauYannis/LS-Projet 📦

An interpreter for an imperative language and a Hoare logic prover

Language: OCaml - Size: 468 KB - Last synced at: 3 months ago - Pushed at: almost 3 years ago - Stars: 0 - Forks: 2

konstantinosKokos/neural-proof-nets 📦

A neural parser for typelogical grammars based on Sinkhorn networks and Linear Logic Proof Nets.

Language: Python - Size: 239 KB - Last synced at: about 2 years ago - Pushed at: over 2 years ago - Stars: 2 - Forks: 1

AbhishekVangipuram/ComputationalProving

Size: 0 Bytes - Last synced at: almost 2 years ago - Pushed at: over 4 years ago - Stars: 0 - Forks: 0

TecMF/GraphProver

A graph based prover.

Language: M4 - Size: 107 KB - Last synced at: almost 2 years ago - Pushed at: over 7 years ago - Stars: 1 - Forks: 0

jacobleygonie/CasualTheoremProver

A kernel using inference rules in order to compute the three of proves.

Language: OCaml - Size: 26.4 KB - Last synced at: almost 2 years ago - Pushed at: over 7 years ago - Stars: 0 - Forks: 0

olbat/robinson-prover

Prover based on Robinson system

Language: Java - Size: 784 KB - Last synced at: 22 days ago - Pushed at: over 13 years ago - Stars: 1 - Forks: 1