#proof-assistant (16 Repositories)
Ranked open-source repositories tagged with #proof-assistant, scored by pull request acceptance likelihood and maintainer engagement velocity.
44.7%
55.4h
16 repositories tagged #proof-assistant
Verified-zkEVM/VCVio
A Lean library for machine-checked cryptographic proofs.
Deducteam/lambdapi
Proof assistant based on the λΠ-calculus modulo rewriting
agda/agda
Agda is a dependently typed programming language / interactive theorem prover.
leanprover-community/LeanProject
A template for blueprint-driven formalization projects in Lean.
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.
epfl-lara/stainless
Verification framework and tool for higher-order Scala programs. https://gitlab.epfl.ch/lara/stainless
rzk-lang/rzk
An experimental proof assistant based on a type theory for synthetic ∞-categories.
verse-lab/veil
A verifier for automated and interactive proofs about transition systems.
engboris/stellogen
An experimental language exploring computation and meaning through term unification, with logic-agnostic types.
aya-prover/aya-dev
A proof assistant and a dependently-typed language
ProofGeneral/PG
This repo is the new home of Proof General
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)
ditto/ditto
A Super Kawaii Dependently Typed Programming Language
RedPRL/redtt
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory