You write everything in Coq. No need to learn a new language. But effects and non-termination are allowed.


You have in hands the full type-system of Coq. You can verify partial correctness properties of your algorithms.


Procedures are extracted to OCaml. Complex results are computed with full speed.

Install with OPAM

Make sure that you added the Coq repository:

opam repo add coq-released

and run:

opam install coq-cybele

Then go to Get started, or explore the Examples.