The Why platform is not any longer under active development. Our effort has moved to the development of Why3.

Why is still maintained, in particular to provide the Jessie plug-in of Frama-C and the Krakatoa front-end for Java. Please refer to the specific web page for Krakatoa and Jessie for more details.

We invite Why users to move to Why3. A quick migration guide is provided. Refer to the Why3 documentation for further details.


Why is a software verification platform.

This platform contains several tools:

One of the main features of Why is to be integrated with many existing provers (proof assistants such as Coq, PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar and decision procedures such as Simplify, Alt-Ergo, Yices, Z3, CVC3, etc.).


User manual, in PostScript and HTML.

Introduction to the Why tool given at the TYPES Summer School 2007 : slides ; lecture notes ; exercises.

Examples of programs certified with Why are collected on this page.

Why is presented in this article. Theoretical foundations are described in this paper.


Why is freely available, under the terms of the GNU LIBRARY GENERAL PUBLIC LICENSE (with a special exception for linking; see the LICENSE file included in the source distribution). It is available as:


There is an Eclipse plugin for Why/Caduceus/Krakatoa.

To download/install theorem provers, look at the Prover Tips page

SMT-lib benchmarks

A set of SMT-lib benchmarks from our test suites: Why Benchmarks.

Related tools

For back-end provers, please look at the Prover Tips page


There is a mailing list for Why (to ask questions about Why, to get announces of new releases, etc.). For bug reports, please use the bug tracking system. For security reasons, you need to register before submitting a new bug. Please create an account there, where you can put "Toccata" for the required field "INRIA Research Project you work with or work in".