Statistics for topic coq

RepositoryStats tracks 569,482 Github repositories, of these 83 are tagged with the coq topic. The most common primary language for repositories using this topic is Coq (51).

Stargazers over time for topic coq

Most starred repositories for topic coq (view more)

coq
coq coq
645
4.8k
lgpl-2.1
104
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive developme...
coq dependent-types proof-assistant theorem-proving
Created 2011-02-17
44,024 commits to master branch, last one a day ago
AbsInt
CompCert AbsInt
226
1.9k
other
63
The CompCert formally-verified C compiler
c coq compcert compiler
Created 2014-09-18
3,150 commits to master branch, last one 4 days ago
UniMath
UniMath UniMath
174
955
other
57
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,254 commits to master branch, last one 17 days ago
Coq-zh
SF-zh Coq-zh
67
919
unknown
53
《软件基础》中译版 Software Foundations Chinese Translation
coq translation chinese-translation
Created 2018-04-04
127 commits to master branch, last one 2 years ago
magmide
magmide magmide
13
811
unknown
51
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 6 months ago
jwiegley
category-theory jwiegley
69
747
bsd-3-clause
20
An axiom-free formalization of category theory in Coq for personal study and practical work
coq monad monoid functor category comonads cartesian categories profunctor construction category-theory profunctor-composition cartesian-closed-category
Created 2014-07-04
1,541 commits to master branch, last one 4 days ago

Trending repositories for topic coq (view more)

Last 3 days (new repositories)
no newly created repositories trending in the last 3 days
Last 3 days (absolute gain)
coq
coq/coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive developme...

4,815 (+3)
lgpl-2.1
jasmin-lang
jasmin-lang/jasmin

Language for high-assurance and high-speed cryptography

262 (+2)
mit
AbsInt
AbsInt/CompCert

The CompCert formally-verified C compiler

1,868 (+2)
coq
coq/vscoq

Visual Studio Code extension for Coq

335 (+1)
mit
PrincetonUniversity
PrincetonUniversity/VST

Verified Software Toolchain

438 (+1)
Last 3 days (relative gain)
jasmin-lang
jasmin-lang/jasmin

Language for high-assurance and high-speed cryptography

262 (+0.8%)
mit
coq
coq/vscoq

Visual Studio Code extension for Coq

335 (+0.3%)
mit
PrincetonUniversity
PrincetonUniversity/VST

Verified Software Toolchain

438 (+0.2%)
jscoq
jscoq/jscoq

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

512 (+0.2%)
AbsInt
AbsInt/CompCert

The CompCert formally-verified C compiler

1,868 (+0.1%)
Last week (new repositories)
no newly created repositories trending in the last week
Last week (absolute gain)
coq
coq/coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive developme...

4,815 (+8)
lgpl-2.1
mit-pdos
mit-pdos/perennial

Verifying concurrent crash-safe systems

153 (+3)
mit
jasmin-lang
jasmin-lang/jasmin

Language for high-assurance and high-speed cryptography

262 (+3)
mit
AbsInt
AbsInt/CompCert

The CompCert formally-verified C compiler

1,868 (+3)
coq
coq/vscoq

Visual Studio Code extension for Coq

335 (+2)
mit
Last week (relative gain)
mit-pdos
mit-pdos/perennial

Verifying concurrent crash-safe systems

153 (+2%)
mit
jasmin-lang
jasmin-lang/jasmin

Language for high-assurance and high-speed cryptography

262 (+1%)
mit
uds-psl
uds-psl/coq-library-undecidability

A library of mechanised undecidability proofs in the Coq proof assistant.

105 (+1.0%)
mpl-2.0
coq
coq/vscoq

Visual Studio Code extension for Coq

335 (+0.6%)
mit
namin
namin/llm-verified-with-monte-carlo-tree-search

LLM verified with Monte Carlo Tree Search

242 (+0.4%)
mit
Last month (new repositories)
no newly created repositories trending in the last month
Last month (absolute gain)
coq
coq/coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive developme...

4,815 (+36)
lgpl-2.1
AbsInt
AbsInt/CompCert

The CompCert formally-verified C compiler

1,868 (+18)
mit-pdos
mit-pdos/perennial

Verifying concurrent crash-safe systems

153 (+11)
mit
jasmin-lang
jasmin-lang/jasmin

Language for high-assurance and high-speed cryptography

262 (+11)
mit
formal-land
formal-land/coq-of-rust

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

405 (+11)
agpl-3.0
Last month (relative gain)
mit-pdos
mit-pdos/perennial

Verifying concurrent crash-safe systems

153 (+8%)
mit
ejgallego
ejgallego/coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq

151 (+5%)
lgpl-2.1
jasmin-lang
jasmin-lang/jasmin

Language for high-assurance and high-speed cryptography

262 (+4%)
mit
namin
namin/llm-verified-with-monte-carlo-tree-search

LLM verified with Monte Carlo Tree Search

242 (+4%)
mit
formal-land
formal-land/coq-of-rust

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

405 (+3%)
agpl-3.0
Last 12-months (new repositories)
namin
namin/llm-verified-with-monte-carlo-tree-search

LLM verified with Monte Carlo Tree Search

242
mit
Last 12-months (absolute gain)
coq
coq/coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive developme...

4,815 (+424)
lgpl-2.1
formal-land
formal-land/coq-of-rust

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

405 (+338)
agpl-3.0
namin
namin/llm-verified-with-monte-carlo-tree-search

LLM verified with Monte Carlo Tree Search

242 (+238)
mit
AbsInt
AbsInt/CompCert

The CompCert formally-verified C compiler

1,868 (+187)
AeneasVerif
AeneasVerif/aeneas

A verification toolchain for Rust programs

182 (+115)
apache-2.0
Last 12-months (relative gain)
namin
namin/llm-verified-with-monte-carlo-tree-search

LLM verified with Monte Carlo Tree Search

242 (+5,950%)
mit
formal-land
formal-land/coq-of-rust

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

405 (+504%)
agpl-3.0
AeneasVerif
AeneasVerif/aeneas

A verification toolchain for Rust programs

182 (+172%)
apache-2.0
IBM
IBM/ACE-RISCV

Assured confidential execution (ACE) implements VM-based trusted execution environment (TEE) for RISC-V with focus on a formally verified and auditable security monitor.

27 (+108%)
apache-2.0
jasmin-lang
jasmin-lang/jasmin

Language for high-assurance and high-speed cryptography

262 (+46%)
mit