Knižnice napísané v Coq e
stalin-sort
Pridajte algoritmus triedenia Stalina v akomkoľvek jazyku, ktorý sa vám páči ❣️ ak chcete, dajte nám ⭐️.
- 1.2k
- MIT
UniMath
Táto knižnica coq má za cieľ formalizovať podstatnú časť matematiky pomocou univalentného uhla pohľadu.
- 853
- GNU General Public License v3.0
magmide
Závisle napísaný dôkazový jazyk určený na to, aby umožnil pracujúcim softvérovým inžinierom preukázateľne správny kód z holého kovu.
- 771
fiat-crypto
Generovanie kryptografického primitívneho kódu od spoločnosti Fiat.
- 594
- GNU General Public License v3.0
CoqGym
Učebné prostredie na dokazovanie teorémov s asistentom dôkazu Coq.
- 332
- GNU Lesser General Public License v3.0 only
verdi-raft
Implementácia distribuovaného konsenzuálneho protokolu Raft, overená v Coq pomocou rámca Verdi.
- 168
- BSD 2-clause "Simplified"
analysis
Knižnica analýzy kompatibilná s matematickými komponentmi (podľa math-comp).
- 158
- GNU General Public License v3.0
fiat
Väčšinou automatizovaná syntéza programov Correct-by-Construction.
- 140
- GNU General Public License v3.0
kami
Platforma pre špecifikáciu parametrického hardvéru na vysokej úrovni a jej modulárne overenie (od mit-plv).
- 126
- MIT
toychain
Minimalistický blockchainový konsenzus implementovaný a overený v Coq.
- 106
- BSD 2-clause "Simplified"
koika
Základný jazyk pre návrh hardvéru založený na pravidlách 🦑.
- 104
- GNU General Public License v3.0 only
silveroak
Formálna špecifikácia a overenie hardvéru, najmä pre bezpečnosť a súkromie.
- 97
- Apache License 2.0
coq-library-undecidability
Knižnica mechanizovaných dôkazov o nerozhodnuteľnosti v Coq dôkazovom asistentovi.
- 96
- GNU General Public License v3.0
vericert
Formálne overený nástroj na syntézu na vysokej úrovni založený na CompCert a napísaný v Coq..
- 71
- GNU General Public License v3.0 only
scala-escape
Doplnok kompilátora na riadenie životnosti objektov v Scale (od TiarkRompf).
- 62
- BSD 3-clause "New" or "Revised"