Bibliotecas escritas em Coq

CompCert

O compilador C formalmente verificado pela CompCert.
  • 1.6k
  • GNU General Public License v3.0

stalin-sort

Adicione um algoritmo stalin sort em qualquer idioma que você goste ❣️ se quiser, dê-nos um ⭐️.
  • 1.2k
  • MIT

Coq-HoTT

Uma biblioteca Coq para a Teoria dos Tipos de Homotopia.
  • 1.2k
  • GNU General Public License v3.0

UniMath

Esta biblioteca coq visa formalizar um corpo substancial de matemática usando o ponto de vista univalente.
  • 853
  • GNU General Public License v3.0

magmide

Uma linguagem de prova de tipagem dependente destinada a tornar o código bare metal comprovadamente correto possível para engenheiros de software.
  • 771

fiat-crypto

Geração de Código Primitivo Criptográfico por Fiat.
  • 594
  • GNU General Public License v3.0

math-comp

Componentes Matemáticos.
  • 501

CoqGym

Um ambiente de aprendizagem para demonstração de teoremas com o assistente de prova Coq.
  • 332
  • GNU Lesser General Public License v3.0 only

sail-riscv

Navegue modelo RISC-V.
  • 306
  • GNU General Public License v3.0

proofs

Meu repositório pessoal de matemática formalmente verificada.
  • 259
  • GNU General Public License v3.0

hacspec

Uma linguagem de especificação para primitivas de criptografia.
  • 218
  • MIT

Coq-Equations

Um pacote de definição de função para Coq.
  • 197
  • GNU Lesser General Public License v3.0 only

verdi-raft

Uma implementação do protocolo de consenso distribuído Raft, verificado em Coq usando a estrutura Verdi.
  • 168
  • BSD 2-clause "Simplified"

jasmin

Linguagem para criptografia de alta segurança e alta velocidade (por jasmin-lang).
  • 159
  • MIT

analysis

Biblioteca de análise compatível com componentes matemáticos (por math-comp).
  • 158
  • GNU General Public License v3.0

fiat

Síntese principalmente automatizada de programas corretos por construção.
  • 140
  • GNU General Public License v3.0

advent-of-coq-2018

Advent of Code 2018, no Coq! (https://adventofcode.com/2018).
  • 139

fourcolor

  • 131
  • GNU General Public License v3.0

kami

Uma plataforma para especificação de hardware paramétrico de alto nível e sua verificação modular (por mit-plv).
  • 126
  • MIT

corn

  • 108
  • GNU General Public License v3.0 only

toychain

Um consenso blockchain minimalista implementado e verificado no Coq.
  • 106
  • BSD 2-clause "Simplified"

koika

Uma linguagem central para design de hardware baseado em regras 🦑.
  • 104
  • GNU General Public License v3.0 only

silveroak

Especificação formal e verificação de hardware, especialmente para segurança e privacidade.
  • 97
  • Apache License 2.0

coq-library-undecidability

Uma biblioteca de provas de indecidibilidade mecanizadas no assistente de prova Coq.
  • 96
  • GNU General Public License v3.0

ConCert

Uma estrutura para verificação de contratos inteligentes em Coq.
  • 92
  • MIT

riscv-coq

Especificação RISC-V em Coq.
  • 87
  • BSD 3-clause "New" or "Revised"

vericert

Uma ferramenta de síntese de alto nível formalmente verificada baseada em CompCert e escrita em Coq..
  • 71
  • GNU General Public License v3.0 only

hs-to-coq

Converta o código-fonte Haskell em código-fonte Coq.
  • 69
  • MIT

scala-escape

Um plug-in de compilador para controlar o tempo de vida do objeto em Scala (por TiarkRompf).
  • 62
  • BSD 3-clause "New" or "Revised"

rupicola

Kit de ferramentas de compilação Gallina para Bedrock2.
  • 46
  • MIT