Statistics for topic coq

RepositoryStats tracks 584,797 Github repositories, of these 85 are tagged with the coq topic. The most common primary language for repositories using this topic is Coq (52).

Stargazers over time for topic coq

Most starred repositories for topic coq (view more)

coq
coq coq
652
4.9k
lgpl-2.1
103
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,367 commits to master branch, last one 20 hours ago
AbsInt
CompCert AbsInt
229
1.9k
other
63
The CompCert formally-verified C compiler
c coq compcert compiler
Created 2014-09-18
3,156 commits to master branch, last one 21 days ago
UniMath
UniMath UniMath
174
961
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,264 commits to master branch, last one 2 days ago
Coq-zh
SF-zh Coq-zh
69
923
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
812
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 7 months ago
jwiegley
category-theory jwiegley
69
754
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,545 commits to master branch, last one 2 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,864 (+3)
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! ✈️ 🚀 ⚕️ 🏦

424 (+2)
agpl-3.0
coq-community
coq-community/awesome-coq

A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainer=@palmskog]

317 (+1)
cc0-1.0
ligurio
ligurio/practical-fm

A gently curated list of companies using verification formal methods in industry

504 (+1)
uwdb
uwdb/Cosette

Cosette is an automated SQL solver.

668 (+1)
bsd-2-clause
Last 3 days (relative gain)
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! ✈️ 🚀 ⚕️ 🏦

424 (+0.5%)
agpl-3.0
coq-community
coq-community/awesome-coq

A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainer=@palmskog]

317 (+0.3%)
cc0-1.0
ligurio
ligurio/practical-fm

A gently curated list of companies using verification formal methods in industry

504 (+0.2%)
uwdb
uwdb/Cosette

Cosette is an automated SQL solver.

668 (+0.1%)
bsd-2-clause
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,864 (+0.1%)
lgpl-2.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,864 (+8)
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! ✈️ 🚀 ⚕️ 🏦

424 (+4)
agpl-3.0
coq-community
coq-community/fourcolor

Formal proof of the Four Color Theorem [maintainer=@ybertot]

167 (+3)
coq-tactician
coq-tactician/coq-tactician

A Seamless, Interactive Tactic Learner and Prover for Coq

59 (+1)
mit
coq
coq/opam

Archive for all Coq related OPAM packages organized in various repositories

126 (+1)
lgpl-2.1
Last week (relative gain)
coq-community
coq-community/fourcolor

Formal proof of the Four Color Theorem [maintainer=@ybertot]

167 (+2%)
coq-tactician
coq-tactician/coq-tactician

A Seamless, Interactive Tactic Learner and Prover for Coq

59 (+2%)
mit
AeneasVerif
AeneasVerif/aeneas

A verification toolchain for Rust programs

199 (+1%)
apache-2.0
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! ✈️ 🚀 ⚕️ 🏦

424 (+1.0%)
agpl-3.0
coq
coq/opam

Archive for all Coq related OPAM packages organized in various repositories

126 (+0.8%)
lgpl-2.1
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,864 (+36)
lgpl-2.1
AbsInt
AbsInt/CompCert

The CompCert formally-verified C compiler

1,891 (+17)
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! ✈️ 🚀 ⚕️ 🏦

424 (+11)
agpl-3.0
AeneasVerif
AeneasVerif/aeneas

A verification toolchain for Rust programs

199 (+10)
apache-2.0
MetaCoq
MetaCoq/metacoq

Metaprogramming, verified meta-theory and implementation of Coq in Coq

382 (+8)
mit
Last month (relative gain)
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.

31 (+7%)
apache-2.0
AeneasVerif
AeneasVerif/aeneas

A verification toolchain for Rust programs

199 (+5%)
apache-2.0
sr-lab
sr-lab/coqpyt

Python client for coq-lsp

26 (+4%)
mit
mit-pdos
mit-pdos/perennial

Verifying concurrent crash-safe systems

163 (+4%)
mit
coq-community
coq-community/fourcolor

Formal proof of the Four Color Theorem [maintainer=@ybertot]

167 (+4%)
Last 12-months (new repositories)
no newly created repositories trending in the last 12 months
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,864 (+440)
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! ✈️ 🚀 ⚕️ 🏦

424 (+349)
agpl-3.0
AbsInt
AbsInt/CompCert

The CompCert formally-verified C compiler

1,891 (+201)
namin
namin/llm-verified-with-monte-carlo-tree-search

LLM verified with Monte Carlo Tree Search

251 (+136)
mit
AeneasVerif
AeneasVerif/aeneas

A verification toolchain for Rust programs

199 (+119)
apache-2.0
Last 12-months (relative gain)
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! ✈️ 🚀 ⚕️ 🏦

424 (+465%)
agpl-3.0
sr-lab
sr-lab/coqpyt

Python client for coq-lsp

26 (+271%)
mit
AeneasVerif
AeneasVerif/aeneas

A verification toolchain for Rust programs

199 (+149%)
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.

31 (+121%)
apache-2.0
namin
namin/llm-verified-with-monte-carlo-tree-search

LLM verified with Monte Carlo Tree Search

251 (+118%)
mit