Simple

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

Safe

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

Efficient

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 https://coq.inria.fr/opam/released

and run:

opam install coq-cybele

Then go to Get started, or explore the Examples.