coq

The Rocq Prover es un demostrador de teoremas interactivo o asistente de pruebas. Proporciona un lenguaje formal para escribir definiciones matemáticas, algoritmos ejecutables y teoremas, junto con un entorno para el desarrollo semiinteractivo de pruebas verificadas por máquina.

El compilador de C verificado formalmente CompCert

Esta biblioteca rocq tiene como objetivo formalizar un cuerpo sustancial de matemáticas utilizando el punto de vista univalente.

Versión en chino de Software Foundations

Una cadena de herramientas de verificación para programas en Rust.

Un lenguaje de prueba con tipos dependientes diseñado para hacer posible el código bare metal demostrablemente correcto para ingenieros de software.

Formalización de la teoría de categorías sin axiomas en Coq para estudio personal y trabajo práctico

Componentes matemáticos.

Cosette es un solucionador automático de SQL.

Un framework para la verificación formal de implementaciones de sistemas distribuidos en Coq

Una lista cuidadosamente seleccionada de empresas que utilizan métodos formales de verificación en la industria.

Este repositorio es el nuevo hogar de Proof General.

Trucos que desearías que el manual de Coq te hubiera contado [maintainer=@tchajed]

Metaprogramación, metateoría verificada e implementación de Rocq en Rocq

Un puerto de Coq a Javascript: ejecuta Coq en tu navegador

Cadena de herramientas de software verificado