用 Coq 编写的库

CompCert

CompCert 经过正式验证的 C 编译器。
  • 1.6k
  • GNU General Public License v3.0

stalin-sort

用您喜欢的任何语言添加斯大林排序算法❣️如果您愿意，请给我们一个⭐️。
  • 1.2k
  • MIT

Coq-HoTT

用于同伦类型理论的 Coq 库。
  • 1.2k
  • GNU General Public License v3.0

UniMath

这个 coq 库旨在使用统一的观点来形式化大量数学。
  • 853
  • GNU General Public License v3.0

magmide

一种依赖类型的证明语言，旨在为工作的软件工程师提供可证明正确的裸机代码。
  • 771

fiat-crypto

菲亚特加密原始代码生成。
  • 594
  • GNU General Public License v3.0

math-comp

数学成分。
  • 501

CoqGym

使用 Coq 证明助手进行定理证明的学习环境。
  • 332
  • GNU Lesser General Public License v3.0 only

sail-riscv

扬帆RISC-V模型。
  • 306
  • GNU General Public License v3.0

proofs

我个人的正式验证数学存储库。
  • 259
  • GNU General Public License v3.0

hacspec

密码学原语的规范语言..
  • 218
  • MIT

Coq-Equations

Coq 的函数定义包。
  • 197
  • GNU Lesser General Public License v3.0 only

verdi-raft

Raft 分布式共识协议的实现，使用 Verdi 框架在 Coq 中进行验证。
  • 168
  • BSD 2-clause "Simplified"

jasmin

用于高保证和高速加密的语言（由 jasmin-lang 提供）。
  • 159
  • MIT

analysis

符合数学组件的分析库（由 math-comp 提供）。
  • 158
  • GNU General Public License v3.0

fiat

主要是构建正确程序的自动合成。
  • 140
  • GNU General Public License v3.0

advent-of-coq-2018

代码 2018 年的到来，在 Coq！ （https://adventofcode.com/2018）。
  • 139

fourcolor

  • 131
  • GNU General Public License v3.0

kami

用于高级参数化硬件规范及其模块化验证的平台（由 mit-plv 提供）。
  • 126
  • MIT

corn

  • 108
  • GNU General Public License v3.0 only

toychain

在 Coq 中实现和验证的简约区块链共识。
  • 106
  • BSD 2-clause "Simplified"

koika

基于规则的硬件设计的核心语言🦑。
  • 104
  • GNU General Public License v3.0 only

silveroak

硬件的正式规范和验证，特别是安全和隐私方面。
  • 97
  • Apache License 2.0

coq-library-undecidability

Coq 证明助手中的机械化不可判定性证明库。
  • 96
  • GNU General Public License v3.0

ConCert

Coq 中的智能合约验证框架。
  • 92
  • MIT

riscv-coq

Coq 中的 RISC-V 规范。
  • 87
  • BSD 3-clause "New" or "Revised"

vericert

一个基于 CompCert 并用 Coq 编写的经过正式验证的高级综合工具。
  • 71
  • GNU General Public License v3.0 only

hs-to-coq

将 Haskell 源代码转换为 Coq 源代码..
  • 69
  • MIT

scala-escape

用于控制 Scala 中对象生命周期的编译器插件（由 TiarkRompf 提供）。
  • 62
  • BSD 3-clause "New" or "Revised"

rupicola

Gallina 到 Bedrock2 编译工具包。
  • 46
  • MIT