Previous Up Next


A computer program is telling the machine how to compute some output from its input. It is not giving the meaning of this computation, nor the reason why the program is correct. In the best case, comments inserted in the code would give part of this information. A formal method gives you the ability to tell the machine both how to compute and why it is correct; hence the name of this tool, Why.

This manual is organized as follows. Chapter 1 gives an overview of Why, illustrating all features with one-line examples. Chapter 2 is a reference manual.


The Why certification tool is © 2002–2014 CNRS/INRIA/Univ Paris-Sud. It is open source and freely available under the terms of the GNU GENERAL PUBLIC LICENSE Version 2. See the files COPYING and GPL in the distribution.


The Why tool is available from, in source and binary formats, together with this documentation and many examples.


There is a mailing list for Why, which is mainly used to announce the releases. See

Bug reports can be sent to

Previous Up Next