proof-assistant
There are 188 repositories under proof-assistant topic.
coq/coq
Coq is a formal proof management system. 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.
FStarLang/FStar
A Proof-oriented Programming Language
agda/agda
Agda is a dependently typed programming language / interactive theorem prover.
plfa/plfa.github.io
An introduction to programming language theory in Agda
ProofGeneral/PG
This repo is the new home of Proof General
jscoq/jscoq
A port of Coq to Javascript -- Run Coq in your Browser
PrincetonUniversity/VST
Verified Software Toolchain
epfl-lara/stainless
Verification framework and tool for higher-order Scala programs
johnyf/tool_lists
Links to tools by subject
cpitclaudel/company-coq
A Coq IDE build on top of Proof General's Coq mode
Deducteam/lambdapi
Proof assistant based on the λΠ-calculus modulo rewriting
aya-prover/aya-dev
A proof assistant and a dependently-typed language
stepchowfun/proofs
My personal repository of formally verified mathematics.
whonore/Coqtail
Interactive Coq Proofs in Vim
latte-central/LaTTe
LaTTe : a Laboratory for Type Theory experiments (in clojure)
rzk-lang/rzk
An experimental proof assistant based on a type theory for synthetic ∞-categories.
RedPRL/sml-redprl
The People's Refinement Logic
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
mit-plv/kami
A Platform for High-Level Parametric Hardware Specification and its Modular Verification
rocq-archive/coq-serapi
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
philzook58/knuckledragger
A Low Barrier Proof Assistant
andrew-johnson-4/LSTS
Large Scale Type Systems (programming language)
engboris/stellogen
An experimental unification-based programming language with logic-agnostic types, based on Girard's transcendental syntax
homotopy-io/homotopy-rs
A Rust/WASM implementation of homotopy.io
amintimany/Categories
A formalization of category theory in the Coq proof assistant.
EugeneLoy/coq_jupyter
Jupyter kernel for Coq
AthenaFoundation/athena
Athena is a modern, practical language for proof engineering & natural deduction.
pitmonticone/LeanProject
A template for blueprint-driven formalization projects in Lean.
RyanMarcus/vulcan
A JavaScript propositional logic and resolution library
molikto/mlang
Towards changing things and see if it proofs
owo-lang/OwO
Placeholder for the OwO compiler
lapisla-prover/lapisla-prover
lapisla is a *battery-pluggable* theorem prover and ecosystem designed for everyone. Greetings! 👋
wenkokke/AutoInAgda
Proof automation – for Agda, in Agda.