uwplse/verdi

A framework for formally verifying distributed systems implementations in Coq

Language: Coq - Size: 2.55 MB - Last synced: about 10 hours ago - Pushed: about 11 hours ago - Stars: 575 - Forks: 56

bedrocksystems/BRiCk

Formalization of C++ for verification purposes.

Language: Coq - Size: 76.1 MB - Last synced: about 21 hours ago - Pushed: 2 days ago - Stars: 61 - Forks: 9

UniMath/UniMath

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

Language: Coq - Size: 27.8 MB - Last synced: 4 days ago - Pushed: 4 days ago - Stars: 915 - Forks: 169

Eggy115/Coq

Coq

Language: Coq - Size: 115 KB - Last synced: 7 days ago - Pushed: about 1 year ago - Stars: 2 - Forks: 1

imdea-software/fcsl-pcm

Partial Commutative Monoids

Language: Coq - Size: 615 KB - Last synced: 7 days ago - Pushed: 7 days ago - Stars: 25 - Forks: 10

PrincetonUniversity/VST

Verified Software Toolchain

Language: Coq - Size: 71.9 MB - Last synced: 16 days ago - Pushed: 21 days ago - Stars: 415 - Forks: 88

liyishuai/coq-show

The Show class in Coq

Language: Coq - Size: 7.81 KB - Last synced: 16 days ago - Pushed: almost 4 years ago - Stars: 0 - Forks: 0

SSProve/ssprove

A foundational framework for modular cryptographic proofs in Coq

Language: Coq - Size: 2.88 MB - Last synced: 15 days ago - Pushed: about 1 month ago - Stars: 50 - Forks: 10

coq-community/math-classes

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

Language: Coq - Size: 2.85 MB - Last synced: 15 days ago - Pushed: 24 days ago - Stars: 158 - Forks: 42

vafeiadis/hahn

Hahn: A Coq library

Language: Coq - Size: 350 KB - Last synced: 15 days ago - Pushed: 23 days ago - Stars: 29 - Forks: 15

coq-community/qarith-stern-brocot

Binary rational numbers in Coq [maintainer=@herbelin]

Language: Coq - Size: 394 KB - Last synced: 26 days ago - Pushed: 5 months ago - Stars: 12 - Forks: 4

coq-community/zorns-lemma 📦

Archived since the contents have been moved to the topology repository

Language: Coq - Size: 91.8 KB - Last synced: 26 days ago - Pushed: over 3 years ago - Stars: 6 - Forks: 6

coq-community/corn

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

Language: Coq - Size: 10.7 MB - Last synced: 15 days ago - Pushed: 24 days ago - Stars: 108 - Forks: 43

coq-community/topology

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

Language: Coq - Size: 754 KB - Last synced: 26 days ago - Pushed: 7 months ago - Stars: 46 - Forks: 10

uwplse/coq-plugin-lib

Library of useful utility functions for Coq plugins

Language: OCaml - Size: 528 KB - Last synced: 5 days ago - Pushed: over 1 year ago - Stars: 11 - Forks: 5

coq-community/coqoban

Sokoban (in Coq) [maintainer=@erikmd]

Language: Coq - Size: 202 KB - Last synced: 15 days ago - Pushed: over 1 year ago - Stars: 21 - Forks: 2

boulme/ImpureDemo

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

Language: Coq - Size: 58.6 KB - Last synced: 3 months ago - Pushed: 3 months 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: 3 months ago - Pushed: 3 months 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: 5 days ago - Pushed: 7 months ago - Stars: 23 - Forks: 5

FedericoBruzzone/software-foundations

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

Language: HTML - Size: 8.59 MB - Last synced: 4 months ago - Pushed: 4 months ago - Stars: 1 - Forks: 0

DabrowskiFr/Structure

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

Language: Coq - Size: 17.6 KB - Last synced: 6 months ago - Pushed: about 4 years ago - Stars: 0 - Forks: 0

coq-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: 178 KB - Last synced: 26 days ago - Pushed: about 2 months ago - Stars: 21 - Forks: 6

DistributedComponents/verdi-cheerios 📦

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

Language: Coq - Size: 33.2 KB - Last synced: 9 months ago - Pushed: over 6 years ago - Stars: 1 - Forks: 0

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: 9 months ago - Pushed: over 1 year ago - Stars: 13 - Forks: 4

uwplse/StructTact

Coq utility and tactic library.

Language: Coq - Size: 275 KB - Last synced: 5 days ago - Pushed: 5 months ago - Stars: 21 - Forks: 8

DistributedComponents/disel

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

Language: Coq - Size: 1.23 MB - Last synced: 9 months ago - Pushed: over 1 year ago - Stars: 94 - Forks: 8

validsdp/validsdp

A Coq tactic for proving multivariate inequalities using SDP solvers

Language: Coq - Size: 30.8 MB - Last synced: about 1 month ago - Pushed: 3 months ago - Stars: 9 - Forks: 1

wkolowski/coq-mtl

An mtl-like library for dealing with effects in Coq

Language: Coq - Size: 4.66 MB - Last synced: about 1 year ago - Pushed: almost 2 years ago - Stars: 2 - Forks: 1

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: about 1 year ago - Pushed: about 5 years ago - Stars: 25 - Forks: 2

wkolowski/coq-algs

Formally verified algorithms in Coq: concepts and techniques

Language: Coq - Size: 16.5 MB - Last synced: about 1 year ago - Pushed: over 1 year ago - Stars: 1 - Forks: 1

co-dan/SeLoC

Strong non-interference for fine-grained concurrent programs

Language: Coq - Size: 358 KB - Last synced: about 1 year ago - Pushed: about 2 years ago - Stars: 3 - Forks: 0

lukaszcz/sortalgs

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

Language: Coq - Size: 23.4 KB - Last synced: about 1 year ago - Pushed: over 2 years ago - Stars: 0 - Forks: 0

coq-community/generic-environments

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

Language: Coq - Size: 37.1 KB - Last synced: 16 days ago - Pushed: over 3 years ago - Stars: 6 - Forks: 1

liyishuai/coq-http2

Language: Coq - Size: 160 KB - Last synced: 16 days ago - Pushed: over 5 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: about 1 year ago - Pushed: about 6 years ago - Stars: 3 - Forks: 0