Knihovny napsané v Coq u
stalin-sort
Přidejte algoritmus řazení stalinů v libovolném jazyce, který se vám líbí ❣️, pokud chcete, dejte nám ⭐️.
- 1.2k
- MIT
UniMath
Tato knihovna coq si klade za cíl formalizovat podstatnou část matematiky pomocí univalentního úhlu pohledu.
- 853
- GNU General Public License v3.0
magmide
Závisle napsaný jazyk nátisku, jehož cílem je umožnit pracujícím softwarovým inženýrům prokazatelně správný kód holého kovu.
- 771
fiat-crypto
Generování kryptografického primitivního kódu od společnosti Fiat.
- 594
- GNU General Public License v3.0
CoqGym
Výukové prostředí pro dokazování teorémů s asistentem důkazu Coq.
- 332
- GNU Lesser General Public License v3.0 only
verdi-raft
Implementace distribuovaného konsenzuálního protokolu Raft, ověřená v Coq pomocí frameworku Verdi.
- 168
- BSD 2-clause "Simplified"
analysis
Kompatibilní s matematickými komponenty Analysis Library (podle math-comp).
- 158
- GNU General Public License v3.0
fiat
Většinou automatizovaná syntéza programů Correct-by-Construction.
- 140
- GNU General Public License v3.0
kami
Platforma pro specifikaci parametrického hardwaru na vysoké úrovni a její modulární ověřování (od mit-plv).
- 126
- MIT
toychain
Minimalistický blockchainový konsensus implementovaný a ověřený v Coq.
- 106
- BSD 2-clause "Simplified"
koika
Základní jazyk pro návrh hardwaru založený na pravidlech 🦑.
- 104
- GNU General Public License v3.0 only
silveroak
Formální specifikace a ověření hardwaru, zejména pro bezpečnost a soukromí.
- 97
- Apache License 2.0
coq-library-undecidability
Knihovna mechanizovaných důkazů nerozhodnutelnosti v Coq proof assistant.
- 96
- GNU General Public License v3.0
vericert
Formálně ověřený nástroj pro syntézu na vysoké úrovni založený na CompCert a napsaný v Coq.
- 71
- GNU General Public License v3.0 only
scala-escape
Kompilační plug-in pro řízení životnosti objektů v Scala (od TiarkRompf).
- 62
- BSD 3-clause "New" or "Revised"