proof-assistant
There are 162 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
jscoq/jscoq
A port of Coq to Javascript -- Run Coq in your Browser
ProofGeneral/PG
This repo is the new home of Proof General
PrincetonUniversity/VST
Verified Software Toolchain
johnyf/tool_lists
Links to tools by subject
epfl-lara/stainless
Verification framework and tool for higher-order Scala programs
cpitclaudel/company-coq
A Coq IDE build on top of Proof General's Coq mode
stepchowfun/proofs
My personal repository of formally verified mathematics.
Deducteam/lambdapi
Proof assistant based on the λΠ-calculus modulo rewriting
whonore/Coqtail
Interactive Coq Proofs in Vim
latte-central/LaTTe
LaTTe : a Laboratory for Type Theory experiments (in clojure)
aya-prover/aya-dev
A proof assistant
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
rzk-lang/rzk
An experimental proof assistant based on a type theory for synthetic ∞-categories.
ditto/ditto
A Super Kawaii Dependently Typed Programming Language
mit-plv/kami
A Platform for High-Level Parametric Hardware Specification and its Modular Verification
ejgallego/coq-serapi
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
andrew-johnson-4/LSTS
Large Scale Type Systems (programming language)
amintimany/Categories
A formalization of category theory in the Coq proof assistant.
EugeneLoy/coq_jupyter
Jupyter kernel for Coq
homotopy-io/homotopy-rs
A Rust/WASM implementation of homotopy.io
AthenaFoundation/athena
Athena is a modern, practical language for proof engineering & natural deduction.
molikto/mlang
Towards changing things and see if it proofs
owo-lang/OwO
Placeholder for the OwO compiler
RyanMarcus/vulcan
A JavaScript propositional logic and resolution library
nunchaku-inria/nunchaku
Model finder for higher-order logic
wenkokke/AutoInAgda
Proof automation – for Agda, in Agda.
ivanbakel/hout-prover
A non-interactive proof assistant using the Haskell type system
konn/type-natural
Type-level well-kinded natural numbers.
TOTBWF/muprl
A small NuPRL style proof assistant