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,
- a general-purpose verification condition generator (VCG),
is used as a back-end by other verification tools (see below) but
which can also be used directly to verify programs
(see for instance these examples) ;
- a tool Krakatoa for the verification of Java programs;
- a tool Caduceus for the verification of C programs; note that
Caduceus is somewhat obsolete now and users should turn to
User manual, in
Introduction to the Why tool given at the
TYPES Summer School
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
It is available as:
- to compile the sources, you need OCaml 3.09 (or higher)
- to compile the graphical user interface gwhy (optional but highly
recommended) you also need the
Lablgtk2 library (Note that there is a Debian package, liblablgtk2-ocaml-dev).
- no prover is distributed with Why, you must install at least one supported prover from the list below
- if you are willing to use Coq as a back-end prover, you
need at least Coq version 7.4
There is an
To download/install theorem provers, look at the Prover Tips page
A set of SMT-lib benchmarks from our test suites:
For back-end provers, please look at the Prover Tips page
a tool on top of Why and Coq to certify
JML-annotated Java programs, by Claude Marché, Christine Paulin, Nicolas Rousset and Xavier Urbain
a tool on top of Why to certify
C programs, by
Filliâtre, Thierry Hubert and Claude Marché ;
now obsolete and subsumed by Frama-C
a general environment for static analysis of C programs, which uses Why has a plugin (plugin Jessie, by Yannick Moy and Claude Marché)
There is a
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".
The main developers of the Why platform are
Also have contributed to development:
Romain Bardou, Jean-François Couchot, Mehdi Dogguy, Christine Paulin, Yann Régis-Gianas, Xavier Urbain
- Yasuhiko Minamide developped the output for Isabelle/HOL
- Seungkeol Choe developped the output for HOL 4
Useful feedback was provided by
M. Levy, N. Magaud, C. Paulin, S. Ranise, L. Théry,
X. Urbain, F. Wiedijk, S. Boldo, G. Melquiond, ... (sorry for the ones we forget to mention)
Levy and César Muñoz contributed to Why's PVS library