Toccata

Logiciels

CFML is a tool that allows to verify the full functional correctness of OCaml programs. Proofs are conducted interactively, within the Coq proof assistant. CFML, which is based on the technique of "characteristic formulae", has been used to verify a collection of data structures and algorithms.
Creusot: an environment for deductive verification of Rust programs
Cubicle: an SMT-based model checker for parameterized systems
Frama-C: Environment for Static Analysis of C source, developed in collaboration with CEA-List and now mainly developed and maintained by CEA
SPARK2014: Environment for the safe development of critical applications in Ada, developed by AdaCore. We contribute to the proof tool of SPARK2014, in the context of the ProofInUse common laboratory.
Why3: A multi-input multi-prover verification platform

Alt-Ergo: automatic prover modulo theories term rewriting toolbox
Gappa is a tool for automatically verifying properties on numerical programs dealing with floating-point or fixed-point arithmetic. While it is intended to be used directly, it can also act as a backend prover for the Why platform or as an automatic tactic for the Coq proof assistant.

ALEA: a Coq library for reasoning on randomized algorithms
Coccinelle: a Coq library for term rewriting systems
Coq.Interval provides a Coq tactic for automatically proving some inequalities between real-valued expressions containing elementary functions.
Coquelicot Coquelicot is a Coq library dedicated to real analysis: differentiation, integration, and so on. It is a conservative extension of the standard library of Coq, but with a strong focus on usability.
Flocq (Floats for Coq) is a formalization of floating-point arithmetic for the Coq system. It provides a comprehensive library of theorems on a multi-radix multi-precision arithmetic; it also supports efficient numerical computations inside Coq.
PFF: a Coq library on floating-point arithmetic