Statistics for language Coq

RepositoryStats tracks 638,232 Github repositories, of these 112 are reported to use a primary language of Coq.

Most starred repositories for language Coq (view more)

AbsInt
CompCert AbsInt
234
2.0k
other
62
The CompCert formally-verified C compiler
c coq compcert compiler
Created 2014-09-18
3,209 commits to master branch, last one 22 days ago
gustavo-depaula
stalin-sort gustavo-depaula
181
1.6k
mit
10
Add a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️
stalin-sort hacktoberfest
Created 2018-10-30
536 commits to master branch, last one about a month ago
HoTT
Coq-HoTT HoTT
197
1.3k
other
59
A Coq library for Homotopy Type Theory
type-theory homotopy-type-theory univalent-foundations
Created 2011-03-26
7,232 commits to master branch, last one a day ago
UniMath
UniMath UniMath
175
976
other
56
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
coq unimath coq-library foundations mathematics
Created 2014-03-01
10,332 commits to master branch, last one a day ago
formal-land
coq-of-rust formal-land
31
888
agpl-3.0
13
Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications! ✈️ 🚀 ⚕️ 🏦
coq rust proof formal-verification
Created 2022-12-28
2,747 commits to main branch, last one 2 days ago
magmide
magmide magmide
13
823
unknown
52
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
coq logic type-safety verification formal-methods dependent-types formal-verification systems-programming
Created 2020-08-21
195 commits to main branch, last one about a year ago

Trending repositories for language Coq (view more)

Last 3 days (new repositories)
no newly created repositories trending in the last 3 days
Last 3 days (absolute gain)
formal-land
formal-land/coq-of-rust

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications! ✈️ 🚀 ⚕️ 🏦

888 (+7)
agpl-3.0
math-comp
math-comp/analysis

Mathematical Components compliant Analysis Library

217 (+3)
PrincetonUniversity
PrincetonUniversity/VST

Verified Software Toolchain

460 (+1)
Last 3 days (relative gain)
math-comp
math-comp/analysis

Mathematical Components compliant Analysis Library

217 (+1%)
formal-land
formal-land/coq-of-rust

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications! ✈️ 🚀 ⚕️ 🏦

888 (+0.8%)
agpl-3.0
PrincetonUniversity
PrincetonUniversity/VST

Verified Software Toolchain

460 (+0.2%)
Last week (new repositories)
no newly created repositories trending in the last week
Last week (absolute gain)
formal-land
formal-land/coq-of-rust

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications! ✈️ 🚀 ⚕️ 🏦

888 (+17)
agpl-3.0
CertiCoq
CertiCoq/certicoq

A Verified Compiler for Gallina, Written in Gallina

148 (+7)
mit
math-comp
math-comp/math-comp

Mathematical Components

612 (+4)
gustavo-depaula
gustavo-depaula/stalin-sort

Add a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️

1,581 (+3)
mit
AbsInt
AbsInt/CompCert

The CompCert formally-verified C compiler

1,959 (+3)
Last week (relative gain)
CertiCoq
CertiCoq/certicoq

A Verified Compiler for Gallina, Written in Gallina

148 (+5%)
mit
formal-land
formal-land/coq-of-rust

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications! ✈️ 🚀 ⚕️ 🏦

888 (+2%)
agpl-3.0
math-comp
math-comp/analysis

Mathematical Components compliant Analysis Library

217 (+0.9%)
ilyasergey
ilyasergey/pnp

Lecture notes for a short course on proving/programming in Coq via SSReflect.

163 (+0.6%)
bsd-2-clause
barry-jay-personal
barry-jay-personal/tree-calculus

Proofs in Coq for the book Reflective Programs in Tree Calculus

170 (+0.6%)
mit
Last month (new repositories)
no newly created repositories trending in the last month
Last month (absolute gain)
formal-land
formal-land/coq-of-rust

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications! ✈️ 🚀 ⚕️ 🏦

888 (+397)
agpl-3.0
AbsInt
AbsInt/CompCert

The CompCert formally-verified C compiler

1,959 (+14)
gustavo-depaula
gustavo-depaula/stalin-sort

Add a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️

1,581 (+12)
mit
mit-plv
mit-plv/fiat-crypto

Cryptographic Primitive Code Generation by Fiat

752 (+9)
CertiCoq
CertiCoq/certicoq

A Verified Compiler for Gallina, Written in Gallina

148 (+7)
mit
Last month (relative gain)
formal-land
formal-land/coq-of-rust

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications! ✈️ 🚀 ⚕️ 🏦

888 (+81%)
agpl-3.0
logsem
logsem/iris-tutorial

No description

50 (+11%)
mit
CertiCoq
CertiCoq/certicoq

A Verified Compiler for Gallina, Written in Gallina

148 (+5%)
mit
bluerock-io
bluerock-io/BRiCk

Formalization of C++ for verification purposes.

80 (+4%)
imdea-software
imdea-software/htt

Hoare Type Theory

74 (+3%)
apache-2.0
Last 12-months (new repositories)
ccz181078
ccz181078/Coq-BB5

No description

191
formal-land
formal-land/coq-of-python

Translate Python code to Coq code for formal verification. Applied to the reference implementation of Ethereum in Python.

33
mit
Last 12-months (absolute gain)
formal-land
formal-land/coq-of-rust

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications! ✈️ 🚀 ⚕️ 🏦

888 (+763)
agpl-3.0
AbsInt
AbsInt/CompCert

The CompCert formally-verified C compiler

1,959 (+201)
ccz181078
ccz181078/Coq-BB5

No description

191 (+190)
gustavo-depaula
gustavo-depaula/stalin-sort

Add a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️

1,581 (+124)
mit
barry-jay-personal
barry-jay-personal/tree-calculus

Proofs in Coq for the book Reflective Programs in Tree Calculus

170 (+120)
mit
Last 12-months (relative gain)
logsem
logsem/iris-tutorial

No description

50 (+733%)
mit
formal-land
formal-land/coq-of-rust

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications! ✈️ 🚀 ⚕️ 🏦

888 (+610%)
agpl-3.0
barry-jay-personal
barry-jay-personal/tree-calculus

Proofs in Coq for the book Reflective Programs in Tree Calculus

170 (+240%)
mit
meithecatte
meithecatte/busycoq

Busy Beaver deciders backed by Coq proof

48 (+220%)
mit
awslabs
awslabs/aws-lc-verification

This repository contains specifications, proof scripts, and other artifacts required to formally verify portions of AWS libcrypto. Formal verification is used to locate bugs and increase assurance of ...

40 (+90%)
apache-2.0