Biblioteker skrevet i Coq

CompCert

CompCert formelt verificerede C compiler.
  • 1.6k
  • GNU General Public License v3.0

stalin-sort

Tilføj en stalin-sorteringsalgoritme på ethvert sprog, du kan lide ❣️ hvis du vil, giv os en ⭐️.
  • 1.2k
  • MIT

Coq-HoTT

Et Coq-bibliotek for Homotopy Type Theory.
  • 1.2k
  • GNU General Public License v3.0

UniMath

Dette coq-bibliotek har til formål at formalisere en betydelig mængde af matematik ved at bruge det univalente synspunkt.
  • 853
  • GNU General Public License v3.0

magmide

Et afhængigt skrevet korrektursprog beregnet til at muliggøre beviseligt korrekt bar metal-kode for arbejdende softwareingeniører.
  • 771

fiat-crypto

Kryptografisk primitiv kodegenerering af Fiat.
  • 594
  • GNU General Public License v3.0

math-comp

Matematiske komponenter.
  • 501

CoqGym

Et læringsmiljø for sætningsbevis med Coq-bevisassistenten.
  • 332
  • GNU Lesser General Public License v3.0 only

sail-riscv

Sejl RISC-V model.
  • 306
  • GNU General Public License v3.0

proofs

Mit personlige lager af formelt bekræftet matematik..
  • 259
  • GNU General Public License v3.0

hacspec

Et specifikationssprog for kryptografiske primitiver..
  • 218
  • MIT

Coq-Equations

En funktionsdefinitionspakke til Coq.
  • 197
  • GNU Lesser General Public License v3.0 only

verdi-raft

En implementering af Rafts distribuerede konsensusprotokol, verificeret i Coq ved hjælp af Verdi-rammen.
  • 168
  • BSD 2-clause "Simplified"

jasmin

Sprog til høj sikkerhed og højhastighedskryptering (af jasmin-lang).
  • 159
  • MIT

analysis

Mathematical Components-kompatibelt Analysebibliotek (ved math-comp).
  • 158
  • GNU General Public License v3.0

fiat

For det meste automatiseret syntese af korrekt-for-konstruktion-programmer.
  • 140
  • GNU General Public License v3.0

advent-of-coq-2018

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

fourcolor

  • 131
  • GNU General Public License v3.0

kami

En platform for parametrisk hardwarespecifikation på højt niveau og dens modulære verifikation (af mit-plv).
  • 126
  • MIT

corn

  • 108
  • GNU General Public License v3.0 only

toychain

En minimalistisk blockchain-konsensus implementeret og verificeret i Coq.
  • 106
  • BSD 2-clause "Simplified"

koika

Et kernesprog til regelbaseret hardwaredesign 🦑.
  • 104
  • GNU General Public License v3.0 only

silveroak

Formel specifikation og verifikation af hardware, især for sikkerhed og privatliv.
  • 97
  • Apache License 2.0

coq-library-undecidability

Et bibliotek med mekaniserede beviser for uafgørlighed i Coq-korrekturassistenten.
  • 96
  • GNU General Public License v3.0

ConCert

En ramme for smart kontraktverifikation i Coq.
  • 92
  • MIT

riscv-coq

RISC-V-specifikation i Coq.
  • 87
  • BSD 3-clause "New" or "Revised"

vericert

Et formelt verificeret synteseværktøj på højt niveau baseret på CompCert og skrevet i Coq..
  • 71
  • GNU General Public License v3.0 only

hs-to-coq

Konverter Haskell kildekode til Coq kildekode..
  • 69
  • MIT

scala-escape

Et compiler-plugin til at styre objektlevetider i Scala (af TiarkRompf).
  • 62
  • BSD 3-clause "New" or "Revised"

rupicola

Gallina til Bedrock2 kompileringsværktøjssæt.
  • 46
  • MIT