Bibliotecas escritas en Coq
CompCert
El compilador de C verificado formalmente por CompCert.
- 1.6k
- GNU General Public License v3.0
stalin-sort
Agregue un algoritmo de clasificación stalin en cualquier idioma que desee ❣️ si lo desea, dénos un ⭐️.
- 1.2k
- MIT
Coq-HoTT
Una biblioteca Coq para la teoría de tipos de homotopía.
- 1.2k
- GNU General Public License v3.0
UniMath
Esta biblioteca coq tiene como objetivo formalizar un cuerpo sustancial de matemáticas utilizando el punto de vista univalente.
- 853
- GNU General Public License v3.0
magmide
Un lenguaje de prueba tipificado de forma dependiente destinado a hacer posible un código bare metal comprobablemente correcto para los ingenieros de software que trabajan.
- 771
fiat-crypto
Generación de código primitivo criptográfico por Fiat.
- 594
- GNU General Public License v3.0
CoqGym
Un entorno de aprendizaje para la demostración de teoremas con el asistente de demostración de Coq.
- 332
- GNU Lesser General Public License v3.0 only
proofs
Mi depósito personal de matemáticas formalmente verificadas.
- 259
- GNU General Public License v3.0
Coq-Equations
Un paquete de definición de funciones para Coq.
- 197
- GNU Lesser General Public License v3.0 only
verdi-raft
Una implementación del protocolo de consenso distribuido Raft, verificado en Coq usando el marco Verdi.
- 168
- BSD 2-clause "Simplified"
analysis
Biblioteca de análisis compatible con componentes matemáticos (por math-comp).
- 158
- GNU General Public License v3.0
fiat
Mayormente síntesis automatizada de programas correctos por construcción.
- 140
- GNU General Public License v3.0
kami
Una plataforma para la especificación de hardware paramétrico de alto nivel y su verificación modular (por mit-plv).
- 126
- MIT
toychain
Un consenso de blockchain minimalista implementado y verificado en Coq.
- 106
- BSD 2-clause "Simplified"
koika
Un lenguaje central para el diseño de hardware basado en reglas 🦑.
- 104
- GNU General Public License v3.0 only
silveroak
Especificación formal y verificación de hardware, especialmente para seguridad y privacidad.
- 97
- Apache License 2.0
coq-library-undecidability
Una biblioteca de pruebas de indecidibilidad mecanizadas en el asistente de pruebas Coq.
- 96
- GNU General Public License v3.0
vericert
Una herramienta de síntesis de alto nivel verificada formalmente basada en CompCert y escrita en Coq..
- 71
- GNU General Public License v3.0 only
scala-escape
Un complemento del compilador para controlar la duración de los objetos en Scala (por TiarkRompf).
- 62
- BSD 3-clause "New" or "Revised"