rooster

Coq.io

Reduce the cost of formally certified programming.

We want to reduce the cost of formal verification in the software industry extending the Coq theorem prover to a programming language.

Language

An extended Gallina to simply programming.

A safe and efficient compiler.

A package manager.