UniMath/UniMath

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

Language: Rocq Prover - Size: 60.3 MB - Last synced at: 1 day ago - Pushed at: 1 day ago - Stars: 984 - Forks: 176

bluerock-io/BRiCk

Formalization of C++ for verification purposes.

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

SSProve/ssprove

A foundational framework for modular cryptographic proofs in Coq

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

PrincetonUniversity/VST

Verified Software Toolchain

Language: Coq - Size: 74.4 MB - Last synced at: about 7 hours ago - Pushed at: about 8 hours 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: 16 days ago - Pushed at: 25 days ago - Stars: 166 - Forks: 43

uwplse/verdi

A framework for formally verifying distributed systems implementations in Coq

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

imdea-software/fcsl-pcm

Partial Commutative Monoids

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

rocq-community/corn

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

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

uwplse/StructTact

Coq utility and tactic library.

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

rocq-community/coqoban

Sokoban (in Coq) [maintainer=@erikmd]

Language: Coq - Size: 203 KB - Last synced at: 2 months ago - Pushed at: 5 months ago - Stars: 20 - 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: 20 days ago - Pushed at: over 2 years ago - Stars: 17 - Forks: 4

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: 2 months ago - Pushed at: 11 months ago - Stars: 98 - Forks: 7

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: about 2 months ago - Pushed at: 4 months ago - Stars: 23 - Forks: 7

rocq-community/qarith-stern-brocot

Binary rational numbers in Coq [maintainer=@herbelin]

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

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

lukaszcz/sortalgs

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

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

rocq-community/topology

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

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

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: 7 days ago - Pushed at: over 4 years ago - Stars: 5 - Forks: 1

vafeiadis/hahn

Hahn: A Coq library

Language: Coq - Size: 350 KB - Last synced at: 26 days ago - Pushed at: 12 months ago - Stars: 30 - Forks: 15

uwplse/coq-plugin-lib

Library of useful utility functions for Coq plugins

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

FedericoBruzzone/software-foundations

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

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

motrellin/comoalg

Some personal notes on typical algebra topics

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

valoran-M/diqt

Formalization of hashtables with Radix trees and PArray in Coq

Language: Coq - Size: 2.19 MB - Last synced at: about 18 hours ago - Pushed at: almost 2 years ago - Stars: 2 - 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

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

uwplse/cheerios

Formally verified Coq serialization library with support for extraction to OCaml

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

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

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: 10 months ago - Pushed at: over 6 years ago - Stars: 28 - Forks: 2

Eggy115/Coq

Coq

Language: Coq - Size: 115 KB - Last synced at: about 2 months ago - Pushed at: about 2 years ago - Stars: 2 - 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: 20 days ago - Pushed at: over 4 years ago - Stars: 6 - Forks: 6

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

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

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: over 2 years ago - Stars: 1 - Forks: 1

co-dan/SeLoC

Strong non-interference for fine-grained concurrent programs

Language: Coq - Size: 358 KB - Last synced at: 2 months ago - Pushed at: about 3 years ago - Stars: 3 - 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

liyishuai/coq-http2

Language: Coq - Size: 160 KB - Last synced at: 2 months ago - Pushed at: over 6 years ago - Stars: 4 - 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