UniMath/UniMath

This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.

Language: Rocq Prover - Size: 61.2 MB - Last synced at: 2 days ago - Pushed at: 9 days ago - Stars: 985 - Forks: 178

uwplse/verdi

A framework for formally verifying distributed systems implementations in Coq

Language: Coq - Size: 2.55 MB - Last synced at: 26 days ago - Pushed at: about 1 year ago - Stars: 606 - Forks: 56

PrincetonUniversity/VST

Verified Software Toolchain

Language: Coq - Size: 74.8 MB - Last synced at: 3 days ago - Pushed at: 3 days ago - Stars: 463 - Forks: 94

rocq-community/math-classes

A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]

Language: Coq - Size: 2.88 MB - Last synced at: 26 days ago - Pushed at: about 1 month ago - Stars: 166 - Forks: 43

rocq-community/corn

Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]

Language: Coq - Size: 10.8 MB - Last synced at: 26 days ago - Pushed at: 5 months ago - Stars: 115 - Forks: 46

DistributedComponents/disel

Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq

Language: Coq - Size: 1.24 MB - Last synced at: 3 months ago - Pushed at: 11 months ago - Stars: 98 - Forks: 7

bluerock-io/BRiCk

Formalization of C++ for verification purposes.

Language: Rocq Prover - Size: 90 MB - Last synced at: about 22 hours ago - Pushed at: about 23 hours ago - Stars: 81 - Forks: 13

SSProve/ssprove

A foundational framework for modular cryptographic proofs in Coq

Language: Coq - Size: 3.31 MB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 64 - Forks: 13

rocq-community/topology

General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]

Language: Coq - Size: 770 KB - Last synced at: about 11 hours ago - Pushed at: 8 months ago - Stars: 48 - Forks: 11

vafeiadis/hahn

Hahn: A Coq library

Language: Coq - Size: 350 KB - Last synced at: about 1 month ago - Pushed at: 12 months ago - Stars: 30 - Forks: 15

imdea-software/fcsl-pcm

Partial Commutative Monoids

Language: Coq - Size: 773 KB - Last synced at: 11 days ago - Pushed at: about 1 month ago - Stars: 28 - Forks: 13

llee454/functional-algebra

This package provides a Coq formalization of abstract algebra using a functional programming style. The modules contained within the package span monoids, groups, rings, and fields and provides both axiom definitions for these structures and proofs of foundational results. The current package contains over 800 definitions and proofs.

Language: Coq - Size: 1.95 MB - Last synced at: 11 months ago - Pushed at: over 6 years ago - Stars: 28 - Forks: 2

rocq-community/bits

A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]

Language: Coq - Size: 188 KB - Last synced at: 2 months ago - Pushed at: 4 months ago - Stars: 23 - Forks: 7

uwplse/StructTact

Coq utility and tactic library.

Language: Coq - Size: 275 KB - Last synced at: 2 months ago - Pushed at: over 1 year ago - Stars: 23 - Forks: 8

uwplse/cheerios

Formally verified Coq serialization library with support for extraction to OCaml

Language: Coq - Size: 370 KB - Last synced at: 2 months ago - Pushed at: over 1 year ago - Stars: 23 - Forks: 5

rocq-community/coqoban

Sokoban (in Coq) [maintainer=@erikmd]

Language: Coq - Size: 203 KB - Last synced at: 9 days ago - Pushed at: 6 months ago - Stars: 22 - Forks: 2

DistributedComponents/InfSeqExt

A Coq library for reasoning (co)inductively on infinite sequences using LTL-like modal operators

Language: Coq - Size: 88.9 KB - Last synced at: about 1 month ago - Pushed at: over 2 years ago - Stars: 17 - Forks: 4

rocq-community/qarith-stern-brocot

Binary rational numbers in Coq [maintainer=@herbelin]

Language: Coq - Size: 394 KB - Last synced at: 2 months ago - Pushed at: over 1 year ago - Stars: 14 - Forks: 4

uwplse/coq-plugin-lib

Library of useful utility functions for Coq plugins

Language: OCaml - Size: 606 KB - Last synced at: 2 months ago - Pushed at: 11 months ago - Stars: 13 - Forks: 5

validsdp/validsdp

A Coq tactic for proving multivariate inequalities using SDP solvers

Language: Coq - Size: 30.9 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 10 - Forks: 1

rocq-community/zorns-lemma 📦

Archived since the contents have been moved to the topology repository

Language: Coq - Size: 91.8 KB - Last synced at: about 1 month ago - Pushed at: over 4 years ago - Stars: 6 - Forks: 6

rocq-community/generic-environments

Coq library that provides an abstract data type for environments [maintainer=@aerabi]

Language: Coq - Size: 37.1 KB - Last synced at: about 10 hours ago - Pushed at: over 4 years ago - Stars: 5 - Forks: 1

liyishuai/coq-http2

Language: Coq - Size: 160 KB - Last synced at: 3 months ago - Pushed at: over 6 years ago - Stars: 4 - Forks: 0

boulme/Impure

A Coq library to embed Impure OCaml oracles in certified Coq code

Language: Coq - Size: 35.2 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 3 - Forks: 0

co-dan/SeLoC

Strong non-interference for fine-grained concurrent programs

Language: Coq - Size: 358 KB - Last synced at: 3 months ago - Pushed at: over 3 years ago - Stars: 3 - Forks: 0

cogumbreiro/aniceto-coq

Aniceto is a library that helps Coq development. It includes a libray of properties on graph theory.

Language: Coq - Size: 248 KB - Last synced at: about 2 years ago - Pushed at: about 7 years ago - Stars: 3 - Forks: 0

valoran-M/diqt

Formalization of hashtables with Radix trees and PArray in Coq

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

Eggy115/Coq

Coq

Language: Coq - Size: 115 KB - Last synced at: 2 months ago - Pushed at: about 2 years ago - Stars: 2 - Forks: 1

wkolowski/coq-mtl

An mtl-like library for dealing with effects in Coq

Language: Coq - Size: 4.66 MB - Last synced at: over 2 years ago - Pushed at: almost 3 years ago - Stars: 2 - Forks: 1

lukaszcz/sortalgs

Various sorting algorithms formalised using the "sauto" component of CoqHammer 1.3.

Language: Coq - Size: 23.4 KB - Last synced at: 4 months ago - Pushed at: over 3 years ago - Stars: 2 - Forks: 0

FedericoBruzzone/software-foundations

Solutions (in Coq) of the exercises in the software foundation books.

Language: HTML - Size: 8.59 MB - Last synced at: 19 days ago - Pushed at: 10 months ago - Stars: 1 - Forks: 0

boulme/ImpureDemo

A Coq library to embed Impure OCaml oracles in certified Coq code

Language: Coq - Size: 58.6 KB - Last synced at: over 1 year ago - Pushed at: over 1 year ago - Stars: 1 - Forks: 0

wkolowski/coq-algs

Formally verified algorithms in Coq: concepts and techniques

Language: Coq - Size: 16.5 MB - Last synced at: over 2 years ago - Pushed at: almost 3 years ago - Stars: 1 - Forks: 1

DistributedComponents/verdi-cheerios 📦

A verified system transformer for serialization of Verdi systems using the Cheerios library.

Language: Coq - Size: 33.2 KB - Last synced at: 3 months ago - Pushed at: almost 8 years ago - Stars: 1 - Forks: 0

motrellin/comoalg

Some personal notes on typical algebra topics

Language: Coq - Size: 87.9 KB - Last synced at: 15 days ago - Pushed at: 11 months ago - Stars: 0 - Forks: 0

liyishuai/coq-show

The Show class in Coq

Language: Coq - Size: 7.81 KB - Last synced at: about 2 months ago - Pushed at: about 5 years ago - Stars: 0 - Forks: 0

DabrowskiFr/Structure

A library of mathematical structures based on type classes proposed in Haskell

Language: Coq - Size: 17.6 KB - Last synced at: over 1 year ago - Pushed at: about 5 years ago - Stars: 0 - Forks: 0

cogumbreiro/aniceto-coq

Aniceto is a library that helps Coq development. It includes a libray of properties on graph theory.

Last synced at: over 2 years ago - Stars: 0 - Forks: 0