Biblioteke napisane u Coq u
stalin-sort
Dodajte staljinov algoritam sortiranja na bilo kojem jeziku koji želite ❣️ ako želite dajte nam ⭐️.
- 1.2k
- MIT
UniMath
Ova biblioteka coq ima za cilj formalizirati značajan dio matematike koristeći jednoznačno gledište.
- 853
- GNU General Public License v3.0
magmide
Zavisno utipkani probni jezik namijenjen da omogući dokazano ispravan goli metalni kod za zaposlene softverske inženjere.
- 771
fiat-crypto
Fiatovo generiranje kriptografskog primitivnog koda.
- 594
- GNU General Public License v3.0
CoqGym
Okruženje za učenje za dokazivanje teorema s Coq pomoćnikom za dokazivanje.
- 332
- GNU Lesser General Public License v3.0 only
verdi-raft
Implementacija Raft distribuiranog konsenzusnog protokola, verificirana u Coqu korištenjem Verdi okvira.
- 168
- BSD 2-clause "Simplified"
analysis
Biblioteka analize usklađena s matematičkim komponentama (math-comp).
- 158
- GNU General Public License v3.0
fiat
Uglavnom automatizirana sinteza programa ispravnih konstrukcija.
- 140
- GNU General Public License v3.0
kami
Platforma za parametarsku specifikaciju hardvera visoke razine i njegovu modularnu provjeru (od strane mit-plv).
- 126
- MIT
toychain
Minimalistički blockchain konsenzus implementiran i verificiran u Coq-u.
- 106
- BSD 2-clause "Simplified"
koika
Temeljni jezik za dizajn hardvera temeljen na pravilima 🦑.
- 104
- GNU General Public License v3.0 only
silveroak
Formalna specifikacija i provjera hardvera, posebno za sigurnost i privatnost..
- 97
- Apache License 2.0
coq-library-undecidability
Knjižnica mehaniziranih dokaza neodlučnosti u pomoćniku za dokazivanje Coq..
- 96
- GNU General Public License v3.0
vericert
Formalno verificirani alat za sintezu visoke razine temeljen na CompCertu i napisan u Coq..
- 71
- GNU General Public License v3.0 only
scala-escape
Dodatak kompajlera za kontrolu životnog vijeka objekta u Scali (autor TiarkRompf).
- 62
- BSD 3-clause "New" or "Revised"