chendamere/UL_ProofAssistance

a proof assistance for Universal Language, a language for proving and forming concepts from data-structure operations. (learn more at the book The Way Of Machine Thinking by Weili Chen)

Language: TeX - Size: 33.8 MB - Last synced at: about 13 hours ago - Pushed at: about 14 hours ago - Stars: 0 - Forks: 0

jaalonso/jaalonso.github.io

Índice de repositorios.

Language: HTML - Size: 70.5 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 1 - Forks: 0

epfl-lara/stainless

Verification framework and tool for higher-order Scala programs

Language: Scala - Size: 139 MB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 374 - Forks: 56

agda/agda

Agda is a dependently typed programming language / interactive theorem prover.

Language: Haskell - Size: 146 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 2,627 - Forks: 369

pitmonticone/LeanProject

Template for blueprint-driven formalization projects in Lean.

Language: Python - Size: 113 KB - Last synced at: 4 days ago - Pushed at: 13 days ago - Stars: 49 - Forks: 5

FStarLang/FStar

A Proof-oriented Programming Language

Language: F* - Size: 752 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 2,835 - Forks: 239

Deducteam/lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting

Language: OCaml - Size: 39.1 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 325 - Forks: 36

philzook58/knuckledragger

A Low Barrier Proof Assistant

Language: Python - Size: 7.5 MB - Last synced at: 5 days ago - Pushed at: 5 days ago - Stars: 109 - Forks: 5

nunchaku-inria/nunchaku

Model finder for higher-order logic

Language: OCaml - Size: 3.98 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 44 - Forks: 3

data61/PSL

Language: Isabelle - Size: 175 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 68 - Forks: 9

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.

Language: OCaml - Size: 195 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 5,084 - Forks: 682

aya-prover/aya-dev

A proof assistant and a dependently-typed language

Language: Java - Size: 18 MB - Last synced at: about 3 hours ago - Pushed at: about 4 hours ago - Stars: 316 - Forks: 19

verse-lab/veil

A verifier for automated and interactive proofs about transition systems. This repository is a public mirror with stable development snapshots. Submit issues and PRs here.

Language: Lean - Size: 1.45 MB - Last synced at: 9 days ago - Pushed at: 9 days ago - Stars: 79 - Forks: 5

groupoid/anders

🧊 Модальний гомотопічний верифікатор математики

Language: OCaml - Size: 14.8 MB - Last synced at: 5 days ago - Pushed at: 10 days ago - Stars: 22 - Forks: 2

lenianiva/Pantograph

(Mirror) A Machine-to-Machine Interaction System for Lean 4

Language: Lean - Size: 956 KB - Last synced at: 5 days ago - Pushed at: 9 days ago - Stars: 20 - Forks: 3

GrahamStrickland/mechanics_of_proof

My own implementation of the exercises and examples in "The Mechanics of Proof" - Heather Macbeth

Language: Lean - Size: 28.3 KB - Last synced at: 10 days ago - Pushed at: 10 days ago - Stars: 0 - Forks: 0

rocq-archive/coq-serapi

Coq Protocol Playground with Se(xp)rialization of Internal Structures.

Language: Coq - Size: 5.82 MB - Last synced at: 1 day ago - Pushed at: 6 months ago - Stars: 130 - Forks: 40

Lambda-Mountain-Compiler-Backend/LSTS

Large Scale Type Systems (programming language)

Size: 1.21 MB - Last synced at: about 12 hours ago - Pushed at: 4 months ago - Stars: 122 - Forks: 3

pqnelson/make-a-hol

Grab a shovel, we're making a HOL

Language: Standard ML - Size: 78.1 KB - Last synced at: 11 days ago - Pushed at: 11 days ago - Stars: 0 - Forks: 0

salastro/deducto

An interactive proof assistant for propositional logic: apply rules; devise premises; and derive conclusions, step-by-step.

Language: Python - Size: 124 KB - Last synced at: 11 days ago - Pushed at: 11 days ago - Stars: 0 - Forks: 1

plfa/plfa.github.io

An introduction to programming language theory in Agda

Language: Agda - Size: 176 MB - Last synced at: 11 days ago - Pushed at: 11 days ago - Stars: 1,420 - Forks: 333

ElNiak/awesome-formal-verification

Welcome to the ultimate list of resources for formal verification techniques and tools. This repository aims to provide an organized collection of high-quality resources to help professionals, researchers, and enthusiasts stay updated and advance their knowledge in the field.

Size: 24.4 KB - Last synced at: 9 days ago - Pushed at: 4 months ago - Stars: 27 - Forks: 2

homotopy-io/homotopy-rs

A Rust/WASM implementation of homotopy.io

Language: Rust - Size: 219 MB - Last synced at: about 16 hours ago - Pushed at: about 17 hours ago - Stars: 96 - Forks: 7

daviddoret/punctilious

A human-friendly and developer-friendly math proof assistant

Language: Python - Size: 55.2 MB - Last synced at: 13 days ago - Pushed at: 13 days ago - Stars: 2 - Forks: 0

PrincetonUniversity/VST

Verified Software Toolchain

Language: Coq - Size: 74.7 MB - Last synced at: 10 days ago - Pushed at: 10 days ago - Stars: 463 - Forks: 93

engboris/stellogen

An experimental unification-based programming language with logic-agnostic types, based on Girard's transcendental syntax

Language: OCaml - Size: 2.06 MB - Last synced at: 6 days ago - Pushed at: 6 days ago - Stars: 101 - Forks: 9

leo-leesco/Computational-Logic-TD4-proof-assistant Fork of smimram/proof-assistant-project

Implementing a proof assistant

Language: OCaml - Size: 50.8 KB - Last synced at: 20 days ago - Pushed at: 20 days ago - Stars: 0 - Forks: 0

ProofGeneral/PG

This repo is the new home of Proof General

Language: Emacs Lisp - Size: 26.3 MB - Last synced at: 20 days ago - Pushed at: 22 days ago - Stars: 511 - Forks: 92

jaalonso/Calculemus2

Proof exercises in Lean4 and Isabelle/HOL

Language: Lean - Size: 16.1 MB - Last synced at: 23 days ago - Pushed at: 23 days ago - Stars: 8 - Forks: 0

Splines/lean-continuous

Continuous functions formalized in Lean4. A students project accompanied by a YouTube video.

Language: TeX - Size: 5.44 MB - Last synced at: 3 days ago - Pushed at: 10 months ago - Stars: 14 - Forks: 2

AthenaFoundation/athena

Athena is a modern, practical language for proof engineering & natural deduction.

Language: Standard ML - Size: 12.6 MB - Last synced at: 22 days ago - Pushed at: 23 days ago - Stars: 71 - Forks: 4

jscoq/jscoq

A port of Coq to Javascript -- Run Coq in your Browser

Language: TypeScript - Size: 14.4 MB - Last synced at: 28 days ago - Pushed at: 7 months ago - Stars: 525 - Forks: 46

stepchowfun/proofs

My personal repository of formally verified mathematics.

Language: Coq - Size: 1.28 MB - Last synced at: 29 days ago - Pushed at: about 2 months ago - Stars: 297 - Forks: 13

EugeneLoy/coq_jupyter

Jupyter kernel for Coq

Language: Python - Size: 414 KB - Last synced at: 5 days ago - Pushed at: 8 months ago - Stars: 95 - Forks: 8

whonore/Coqtail

Interactive Coq Proofs in Vim

Language: Python - Size: 922 KB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 288 - Forks: 36

rzk-lang/rzk

An experimental proof assistant based on a type theory for synthetic ∞-categories.

Language: Haskell - Size: 55.6 MB - Last synced at: 29 days ago - Pushed at: about 2 months ago - Stars: 219 - Forks: 10

altaris/opetopy

Proof assistant for opetope and opetopic set derivation systems :snake: :mortar_board:

Language: Python - Size: 190 KB - Last synced at: 6 days ago - Pushed at: about 5 years ago - Stars: 15 - Forks: 1

TimothyEarley/arend-sandbox

Playing around with Arend

Size: 397 KB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 0 - Forks: 0

JadAbouHawili/Raymond-Smullyan-KnightsAndKnaves

Formalization and solution of knights and knaves puzzles in lean 4

Language: Lean - Size: 137 KB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 2 - Forks: 0

qdeduction/qbar

the rational proof assistant

Language: Rust - Size: 2.49 MB - Last synced at: 2 days ago - Pushed at: almost 2 years ago - Stars: 2 - Forks: 0

Merlin04/truthtabl.es

Truth table generator, (basic) proof builder, and more, built with Next.js and Ohm

Language: TypeScript - Size: 252 KB - Last synced at: 3 days ago - Pushed at: over 1 year ago - Stars: 23 - Forks: 3

cpitclaudel/company-coq

A Coq IDE build on top of Proof General's Coq mode

Language: Emacs Lisp - Size: 22.8 MB - Last synced at: about 1 month ago - Pushed at: over 2 years ago - Stars: 356 - Forks: 28

ivanbakel/hout-prover

A non-interactive proof assistant using the Haskell type system

Language: Haskell - Size: 25.4 KB - Last synced at: 8 days ago - Pushed at: about 5 years ago - Stars: 37 - Forks: 1

mnPanic/tesis

Tesis de licenciatura. DC UBA. PPA - Pani's Proof Assistant

Language: Haskell - Size: 35.5 MB - Last synced at: about 2 months ago - Pushed at: about 2 months ago - Stars: 1 - Forks: 0

mit-plv/kami

A Platform for High-Level Parametric Hardware Specification and its Modular Verification

Language: Coq - Size: 4.67 MB - Last synced at: about 1 month ago - Pushed at: 8 months ago - Stars: 151 - Forks: 26

smimram/decaml

Dependent variant of OCaml

Language: OCaml - Size: 181 KB - Last synced at: 27 days ago - Pushed at: about 2 months ago - Stars: 4 - Forks: 0

forked-from-1kasper/anders

Anders: Cubical Type Checker

Language: OCaml - Size: 4.02 MB - Last synced at: 18 days ago - Pushed at: over 1 year ago - Stars: 24 - Forks: 1

latte-central/LaTTe

LaTTe : a Laboratory for Type Theory experiments (in clojure)

Language: Clojure - Size: 703 KB - Last synced at: 1 day ago - Pushed at: about 2 months ago - Stars: 259 - Forks: 13

RedPRL/redtt

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory

Language: OCaml - Size: 3.02 MB - Last synced at: 16 days ago - Pushed at: about 3 years ago - Stars: 208 - Forks: 12

johnyf/tool_lists

Links to tools by subject

Size: 63.5 KB - Last synced at: about 2 months ago - Pushed at: about 1 year ago - Stars: 375 - Forks: 83

RedPRL/cooltt

😎TT

Language: OCaml - Size: 3.48 MB - Last synced at: about 1 month ago - Pushed at: over 1 year ago - Stars: 225 - Forks: 14

pitmonticone/LeanCHANGE

Repository hosting the resources for the Lean demo session of my talk presented at the weekly research seminar on CHallenges in ANalysis and GEometry (CHANGE) at the University of Trento on February 11, 2025.

Language: Lean - Size: 1.23 MB - Last synced at: 4 days ago - Pushed at: 3 months ago - Stars: 3 - Forks: 0

FlorianCassayre/master-project

Master Thesis Project at LARA (EPFL)

Language: Scala - Size: 940 KB - Last synced at: 5 days ago - Pushed at: almost 3 years ago - Stars: 3 - Forks: 0

RedPRL/algaett

🦠 An experimental elaborator for dependent type theory using effects and handlers

Language: OCaml - Size: 620 KB - Last synced at: 16 days ago - Pushed at: over 1 year ago - Stars: 35 - Forks: 0

SReichelt/slate

The Slate Interactive Theorem Prover

Language: TypeScript - Size: 7.5 MB - Last synced at: about 2 months ago - Pushed at: over 2 years ago - Stars: 24 - Forks: 2

daviromero/nadia

Natural Deduction Proof Assistant (NADIA) is a tool for teaching Natural Deduction in Fitch-Style

Language: Python - Size: 206 KB - Last synced at: 19 days ago - Pushed at: over 1 year ago - Stars: 30 - Forks: 0

HOLMS-lib/HOLMS

HOL-Light Library for Modal Systems

Language: OCaml - Size: 212 KB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 1 - Forks: 0

lapisla-prover/lapisla-prover

Lapisla is a *battery-pluggable* theorem prover and ecosystem designed for everyone. Greetings! 👋

Language: TypeScript - Size: 9.76 MB - Last synced at: 2 months ago - Pushed at: 2 months ago - Stars: 46 - Forks: 2

appliedfm/vstyle

A style guide for Coq

Size: 646 KB - Last synced at: about 1 month ago - Pushed at: over 3 years ago - Stars: 18 - Forks: 0

konn/type-natural

Type-level well-kinded natural numbers.

Language: Haskell - Size: 555 KB - Last synced at: about 1 month ago - Pushed at: 4 months ago - Stars: 34 - Forks: 12

forked-from-1kasper/bravo

Castle Bravo: Experimental HoTT Implementation

Language: OCaml - Size: 381 KB - Last synced at: 18 days ago - Pushed at: almost 2 years ago - Stars: 7 - Forks: 1

forked-from-1kasper/hurricane

Hurricane: HoTT-I Type System

Language: OCaml - Size: 44.9 KB - Last synced at: 3 months ago - Pushed at: about 3 years ago - Stars: 1 - Forks: 0

amintimany/Categories

A formalization of category theory in the Coq proof assistant.

Language: Coq - Size: 596 KB - Last synced at: 9 days ago - Pushed at: 6 months ago - Stars: 95 - Forks: 4

TOTBWF/muprl

A small NuPRL style proof assistant

Language: Haskell - Size: 110 KB - Last synced at: 27 days ago - Pushed at: over 6 years ago - Stars: 31 - Forks: 1

mit-plv/hemiola

A Coq framework to support structural design and proof of hardware cache-coherence protocols

Language: Coq - Size: 4.94 MB - Last synced at: about 1 month ago - Pushed at: about 3 years ago - Stars: 13 - Forks: 0

h2-math/coq-nahas-tutorial

Coq Tutorial from Mike Nahas's repo at https://github.com/mdnahas/mdnahas.github.io/doc/nahas_tutorial.v

Language: HTML - Size: 216 KB - Last synced at: 2 months ago - Pushed at: 4 months ago - Stars: 0 - Forks: 0

pitmonticone/LeanInVienna2024

Repository hosting resources for the "Lean Tutorial in Vienna" at TU Wien from September 18 to 20, 2024.

Language: Lean - Size: 1.58 MB - Last synced at: 4 days ago - Pushed at: 4 months ago - Stars: 9 - Forks: 2

GrahamStrickland/functional_lean

Examples and exercises from "Functional Programming in Lean" - David Thrane Christiansen

Language: Lean - Size: 31.3 KB - Last synced at: 13 days ago - Pushed at: 4 months ago - Stars: 0 - Forks: 0

annenkov/two-level

Two-Level Type Theory

Language: Lean - Size: 151 KB - Last synced at: 19 days ago - Pushed at: over 5 years ago - Stars: 28 - Forks: 1

smimram/proof-assistant-project

Template for the proof assistant project CSC_51051_EP.

Language: OCaml - Size: 5.86 KB - Last synced at: about 1 month ago - Pushed at: 4 months ago - Stars: 8 - Forks: 23

Matafou/LibHyps

A Coq library providing tactics to deal with hypothesis

Language: Coq - Size: 169 KB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 20 - Forks: 3

HOLMS-lib/holms-lib.github.io

HOL Light Library for Modal Systems

Size: 96.7 KB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 0 - Forks: 0

RedPRL/mugen

♾️ A library for universe levels and universe polymorphism

Language: OCaml - Size: 727 KB - Last synced at: 16 days ago - Pushed at: 5 months ago - Stars: 34 - Forks: 1

philzook58/Knuckledragger.jl

Julia Semi-Automated Proof Assistant

Language: Julia - Size: 4.88 KB - Last synced at: 4 days ago - Pushed at: 6 months ago - Stars: 3 - Forks: 1

RyanMarcus/vulcan

A JavaScript propositional logic and resolution library

Language: JavaScript - Size: 47.9 KB - Last synced at: 6 days ago - Pushed at: over 7 years ago - Stars: 61 - Forks: 8

hauntedhost/programming-language-foundations-in-agda

Programming Language Foundations in Agda by Philip Wadler and Wen Kokke

Language: Agda - Size: 257 KB - Last synced at: 5 months ago - Pushed at: 5 months ago - Stars: 0 - Forks: 0

forked-from-1kasper/romeo

Castle Romeo: Experimental Theorem Prover for Category Theory

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

5eqn/proof-cat

A drag-and-drop proof assistant inspired by Scratch.

Language: TypeScript - Size: 677 KB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 7 - Forks: 0

KonjacSource/ShiTT

ShiTT is a toy proof assistant (almost).

Language: Haskell - Size: 354 KB - Last synced at: 6 months ago - Pushed at: 6 months ago - Stars: 27 - Forks: 1

marigold-dev/easier-proofs

A project which aim to help engineers to make proves easily

Language: OCaml - Size: 265 KB - Last synced at: about 1 month ago - Pushed at: about 3 years ago - Stars: 13 - Forks: 1

proost-assistant/ProostLean

An reimplementation of the Proost proof-assistant written in Lean 4

Language: Lean - Size: 173 KB - Last synced at: 5 months ago - Pushed at: about 1 year ago - Stars: 12 - Forks: 0

EuroProofNet/ATP

Repository of EuroProofNet WG 2 on ATPs

Language: OpenEdge ABL - Size: 28.3 KB - Last synced at: 4 months ago - Pushed at: almost 2 years ago - Stars: 4 - Forks: 1

jaalonso/Calculemus2_es

Ejercicios de demostración con Lean4 e Isabelle/HOL.

Language: Lean - Size: 1.86 MB - Last synced at: 7 months ago - Pushed at: 7 months ago - Stars: 2 - Forks: 0

iskportal/Dedukt

Dedukt is an open source project of software for mathemaical practice using computers. The main goal is to develop a user firendly, intelligent system for mathematics, proof, new mathematical developments, and also symbolic computation. It can be used by mathematicians and people in sciences.

Language: TeX - Size: 275 KB - Last synced at: 3 months ago - Pushed at: 11 months ago - Stars: 3 - Forks: 0

nyuichi/LeanHOL

super tiny implementation of higher-order logic proof assistant in lean

Language: Lean - Size: 21.5 KB - Last synced at: about 2 months ago - Pushed at: over 5 years ago - Stars: 21 - Forks: 0

herulume/Galculator

A functional prototype of a Galois-connection based proof assistant

Language: Haskell - Size: 55.7 KB - Last synced at: about 2 months ago - Pushed at: about 4 years ago - Stars: 2 - Forks: 1

AtticusKuhn/proofs-from-the-book

Proofs from THE BOOK by Aigner and Ziegler proved in the Lean proving assistant

Language: Lean - Size: 181 KB - Last synced at: 30 days ago - Pushed at: over 3 years ago - Stars: 2 - Forks: 0

RedPRL/kado

🧊 kado カド: Cofibrations in Cartesian Cubical Type Theory

Language: OCaml - Size: 648 KB - Last synced at: 16 days ago - Pushed at: 7 months ago - Stars: 19 - Forks: 1

proost-assistant/proost

A small proof assistant written in Rust. Read-only mirror of https://gitlab.crans.org/loutr/proost.

Language: Rust - Size: 1.21 MB - Last synced at: 5 months ago - Pushed at: 9 months ago - Stars: 27 - Forks: 2

spidermoy/tree_sort_verificated

A formal specification and verification of Tree Sort algorithm in Coq

Language: Coq - Size: 11.7 KB - Last synced at: 8 months ago - Pushed at: 8 months ago - Stars: 0 - Forks: 0

surajx/proof-assistant

Online platform to enable Logic students to write, verify, and store System L style Natural Deduction proofs with real-time proof-checking

Language: JavaScript - Size: 1.24 MB - Last synced at: about 1 month ago - Pushed at: almost 7 years ago - Stars: 11 - Forks: 3

amka66/mai

mai: MAth Interpreter with Standard Foundations

Language: Prolog - Size: 177 KB - Last synced at: 8 months ago - Pushed at: 8 months ago - Stars: 4 - Forks: 1

rlepigre/pml

New version of the PML language and (classical) proof assistant

Language: OCaml - Size: 5.78 MB - Last synced at: about 1 month ago - Pushed at: over 2 years ago - Stars: 20 - Forks: 2

mstfelg/barhana

Logic derivation engine in Python

Language: Python - Size: 62.5 KB - Last synced at: 9 months ago - Pushed at: 9 months ago - Stars: 1 - Forks: 0

rzk-lang/vscode-rzk

Visual Studio Code Extension(s) for Rzk proof assistant.

Language: TypeScript - Size: 601 KB - Last synced at: about 1 month ago - Pushed at: 11 months ago - Stars: 8 - Forks: 1

acsd-tu-chemnitz/conformlog

Language: Scheme - Size: 143 KB - Last synced at: 10 months ago - Pushed at: 10 months ago - Stars: 0 - Forks: 1

daviromero/anita

Analytic Tableau Proof Assistant (ANITA) is a tool for teaching Analytic Tableaux

Language: Python - Size: 368 KB - Last synced at: 9 months ago - Pushed at: over 1 year ago - Stars: 19 - Forks: 0

wkolowski/Type-Theory-Wishlist

Personal research notes

Language: Coq - Size: 1.13 MB - Last synced at: 10 months ago - Pushed at: 10 months ago - Stars: 5 - Forks: 0

pitmonticone/carleson Fork of fpvandoorn/carleson

[WIP] A formalised proof of a generalised Carleson's Theorem in the Lean proof assistant.

Language: TeX - Size: 1.31 MB - Last synced at: 11 months ago - Pushed at: 11 months ago - Stars: 0 - Forks: 0

fsestini/nbe-mltt-wes

Normalization by Evaluation for a version of Martin-Löf Type Theory with weak explicit substitutions.

Language: Agda - Size: 26.4 KB - Last synced at: 5 months ago - Pushed at: about 2 years ago - Stars: 6 - Forks: 0