Bibliotek skrivna i Coq
UniMath
Detta coq-bibliotek syftar till att formalisera en stor mängd matematik med hjälp av den univalenta synvinkeln.
- 853
- GNU General Public License v3.0
magmide
Ett beroendetypat korrekturspråk avsett att göra bevisligen korrekt barmetallkod möjlig för arbetande mjukvaruingenjörer.
- 771
proofs
Mitt personliga arkiv med formellt verifierad matematik..
- 259
- GNU General Public License v3.0
Coq-Equations
Ett funktionsdefinitionspaket för Coq.
- 197
- GNU Lesser General Public License v3.0 only
verdi-raft
En implementering av Rafts distribuerade konsensusprotokoll, verifierad i Coq med hjälp av Verdi-ramverket.
- 168
- BSD 2-clause "Simplified"
analysis
Mathematical Components-kompatibel analysbibliotek (av math-comp).
- 158
- GNU General Public License v3.0
kami
En plattform för parametrisk hårdvaruspecifikation på hög nivå och dess modulära verifiering (av mit-plv).
- 126
- MIT
toychain
En minimalistisk blockchain-konsensus implementerad och verifierad i Coq.
- 106
- BSD 2-clause "Simplified"
coq-library-undecidability
Ett bibliotek med mekaniserade bevis för oavgörbarhet i Coq proof assistant..
- 96
- GNU General Public License v3.0
vericert
Ett formellt verifierat syntesverktyg på hög nivå baserat på CompCert och skrivet i Coq..
- 71
- GNU General Public License v3.0 only
