In Coq geschriebene Bibliotheken

CompCert

Der von CompCert offiziell verifizierte C-Compiler.
  • 1.6k
  • GNU General Public License v3.0

stalin-sort

Fügen Sie einen Stalin-Sortieralgorithmus in einer beliebigen Sprache hinzu. ❣️ Wenn Sie möchten, geben Sie uns ein ⭐️.
  • 1.2k
  • MIT

Coq-HoTT

Eine Coq-Bibliothek für die Homotopietypentheorie.
  • 1.2k
  • GNU General Public License v3.0

UniMath

Ziel dieser Coq-Bibliothek ist es, einen umfangreichen Teil der Mathematik unter Verwendung der univalenten Sichtweise zu formalisieren.
  • 853
  • GNU General Public License v3.0

magmide

Eine abhängig typisierte Beweissprache, die arbeitenden Softwareentwicklern nachweislich korrekten Bare-Metal-Code ermöglichen soll.
  • 771

fiat-crypto

Kryptografische Primitivcode-Generierung von Fiat.
  • 594
  • GNU General Public License v3.0

math-comp

Mathematische Komponenten.
  • 501

CoqGym

Eine Lernumgebung für Theorembeweise mit dem Coq-Beweisassistenten.
  • 332
  • GNU Lesser General Public License v3.0 only

sail-riscv

Segel-RISC-V-Modell.
  • 306
  • GNU General Public License v3.0

proofs

Mein persönlicher Fundus an formal verifizierter Mathematik.
  • 259
  • GNU General Public License v3.0

hacspec

Eine Spezifikationssprache für Kryptographieprimitive.
  • 218
  • MIT

Coq-Equations

Ein Funktionsdefinitionspaket für Coq.
  • 197
  • GNU Lesser General Public License v3.0 only

verdi-raft

Eine Implementierung des verteilten Konsensprotokolls Raft, verifiziert in Coq unter Verwendung des Verdi-Frameworks.
  • 168
  • BSD 2-clause "Simplified"

jasmin

Sprache für Hochsicherheits- und Hochgeschwindigkeitskryptographie (von jasmin-lang).
  • 159
  • MIT

analysis

Mit Mathematical Components kompatible Analysebibliothek (von math-comp).
  • 158
  • GNU General Public License v3.0

fiat

Weitgehend automatisierte Synthese von Correct-by-Construction-Programmen.
  • 140
  • GNU General Public License v3.0

advent-of-coq-2018

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

fourcolor

  • 131
  • GNU General Public License v3.0

kami

Eine Plattform für hochrangige parametrische Hardwarespezifikation und deren modulare Verifizierung (von mit-plv).
  • 126
  • MIT

corn

  • 108
  • GNU General Public License v3.0 only

toychain

Ein minimalistischer Blockchain-Konsens, der in Coq implementiert und verifiziert wird.
  • 106
  • BSD 2-clause "Simplified"

koika

Eine Kernsprache für regelbasiertes Hardwaredesign 🦑.
  • 104
  • GNU General Public License v3.0 only

silveroak

Formale Spezifikation und Verifizierung von Hardware, insbesondere für Sicherheit und Datenschutz.
  • 97
  • Apache License 2.0

coq-library-undecidability

Eine Bibliothek mechanisierter Unentscheidbarkeitsbeweise im Coq-Beweisassistenten.
  • 96
  • GNU General Public License v3.0

ConCert

Ein Framework für die Überprüfung intelligenter Verträge in Coq.
  • 92
  • MIT

riscv-coq

RISC-V-Spezifikation in Coq.
  • 87
  • BSD 3-clause "New" or "Revised"

vericert

Ein formal verifiziertes High-Level-Synthese-Tool, das auf CompCert basiert und in Coq. geschrieben ist.
  • 71
  • GNU General Public License v3.0 only

hs-to-coq

Konvertieren Sie Haskell-Quellcode in Coq-Quellcode.
  • 69
  • MIT

scala-escape

Ein Compiler-Plug-in zur Steuerung der Objektlebensdauer in Scala (von TiarkRompf).
  • 62
  • BSD 3-clause "New" or "Revised"

rupicola

Gallina to Bedrock2-Kompilierungs-Toolkit.
  • 46
  • MIT