Biblioteki napisane w Coq

CompCert

Kompilator języka C, który został formalnie zweryfikowany przez CompCert.
  • 1.6k
  • GNU General Public License v3.0

stalin-sort

Dodaj stalinowski algorytm sortowania w dowolnym języku ❣️ jeśli chcesz daj nam ⭐️.
  • 1.2k
  • MIT

Coq-HoTT

Biblioteka Coq dla teorii typów homotopii.
  • 1.2k
  • GNU General Public License v3.0

UniMath

Ta biblioteka coq ma na celu sformalizowanie znacznej części matematyki przy użyciu jednowartościowego punktu widzenia.
  • 853
  • GNU General Public License v3.0

magmide

Język sprawdzający o zależnym typowaniu, mający na celu umożliwienie pracującym inżynierom oprogramowania możliwego do udowodnienia poprawnego kodu bare metal.
  • 771

fiat-crypto

Generowanie prymitywnego kodu kryptograficznego przez Fiata.
  • 594
  • GNU General Public License v3.0

math-comp

Komponenty matematyczne.
  • 501

CoqGym

Środowisko uczenia się do udowadniania twierdzeń z asystentem dowodu Coq.
  • 332
  • GNU Lesser General Public License v3.0 only

sail-riscv

Model żagla RISC-V.
  • 306
  • GNU General Public License v3.0

proofs

Moje osobiste repozytorium formalnie zweryfikowanej matematyki..
  • 259
  • GNU General Public License v3.0

hacspec

Język specyfikacji dla prymitywów kryptograficznych.
  • 218
  • MIT

Coq-Equations

Pakiet definicji funkcji dla Coq.
  • 197
  • GNU Lesser General Public License v3.0 only

verdi-raft

Implementacja rozproszonego protokołu konsensusu Raft, zweryfikowana w Coq przy użyciu frameworka Verdi.
  • 168
  • BSD 2-clause "Simplified"

jasmin

Język dla wysokiej pewności i szybkiej kryptografii (autor: jasmin-lang).
  • 159
  • MIT

analysis

Biblioteka analiz zgodna z komponentami matematycznymi (przez math-comp).
  • 158
  • GNU General Public License v3.0

fiat

W większości zautomatyzowana synteza programów poprawnych przez konstrukcję.
  • 140
  • GNU General Public License v3.0

advent-of-coq-2018

Nadejście Kodeksu 2018 w Coq! (https://adventofcode.com/2018).
  • 139

fourcolor

  • 131
  • GNU General Public License v3.0

kami

Platforma parametrycznej specyfikacji sprzętu wysokiego poziomu i jej modułowej weryfikacji (autor: mit-plv).
  • 126
  • MIT

corn

  • 108
  • GNU General Public License v3.0 only

toychain

Minimalistyczny konsensus blockchain zaimplementowany i zweryfikowany w Coq.
  • 106
  • BSD 2-clause "Simplified"

koika

Podstawowy język projektowania sprzętu opartego na regułach 🦑.
  • 104
  • GNU General Public License v3.0 only

silveroak

Formalna specyfikacja i weryfikacja sprzętu, szczególnie pod kątem bezpieczeństwa i prywatności.
  • 97
  • Apache License 2.0

coq-library-undecidability

Biblioteka zmechanizowanych dowodów nierozstrzygalności w asystencie dowodu Coq.
  • 96
  • GNU General Public License v3.0

ConCert

Ramy weryfikacji inteligentnych kontraktów w Coq.
  • 92
  • MIT

riscv-coq

Specyfikacja RISC-V w Coq.
  • 87
  • BSD 3-clause "New" or "Revised"

vericert

Formalnie zweryfikowane narzędzie do syntezy wysokiego poziomu oparte na CompCert i napisane w Coq..
  • 71
  • GNU General Public License v3.0 only

hs-to-coq

Konwertuj kod źródłowy Haskella na kod źródłowy Coq.
  • 69
  • MIT

scala-escape

Wtyczka kompilatora do kontrolowania czasu życia obiektów w Scali (autorstwa TiarkRompf).
  • 62
  • BSD 3-clause "New" or "Revised"

rupicola

Gallina do zestawu narzędzi do kompilacji Bedrock2.
  • 46
  • MIT