#proof-assistant (13 Repositories)
Ranked open-source repositories tagged with #proof-assistant, scored by pull request acceptance likelihood and maintainer engagement velocity.
37.3%
84.7h
13 repositories tagged #proof-assistant
Deducteam/lambdapi
Proof assistant based on the λΠ-calculus modulo rewriting
rzk-lang/rzk
An experimental proof assistant based on a type theory for synthetic ∞-categories.
agda/agda
Agda is a dependently typed programming language / interactive theorem prover.
engboris/stellogen
An experimental language exploring computation and meaning through term unification, with logic-agnostic types.
rocq-prover/rocq
The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Verified-zkEVM/VCVio
A Lean library for machine-checked cryptographic proofs.
epfl-lara/stainless
Verification framework and tool for higher-order Scala programs. https://gitlab.epfl.ch/lara/stainless
verse-lab/veil
A verifier for automated and interactive proofs about transition systems.
RedPRL/redtt
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
ditto/ditto
A Super Kawaii Dependently Typed Programming Language
cpitclaudel/company-coq
A Coq IDE build on top of Proof General's Coq mode
latte-central/LaTTe
LaTTe : a Laboratory for Type Theory experiments (in clojure)