### Overview

Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs.Why3 is a complete reimplementation of the former Why platform. Among the new features are: numerous extensions to the input language, a new architecture for calling external provers, and a well-designed API, allowing to use Why3 as a software library. An important emphasis is put on modularity and genericity, giving the end user a possibility to easily reuse Why3 formalizations or to add support for a new external prover if wanted.

See the specific section below for the list of supported provers.

Why3 is developed in the
team-project Toccata
(formerly ProVal) at Inria
Saclay-Île-de-France / LRI Univ Paris-Sud 11 / CNRS.

## Contact |
## Download |
## People |

## Documentation and Examples

- PDF manual (version 0.85)
- Online manual (version 0.85)
- Standard library (version 0.85)
- Online API reference (version 0.85)
- Quick migration guide from Why 2.xx to Why3

### Related Publications

- Logic
- Programming language and Environment
- Applications and Case Studies
- Verifying Two Lines of C with Why3: an Exercise in Program Verification (VSTTE 2012) [bib]
- Discharging Proof Obligations from Atelier B using Multiple Automated Provers [bib]
- Binary heaps formally verified in Why3 [bib]
- Verified programs with binders (PLPV 2014) [bib]
- Let's verify this with Why3 [bib]

### Examples, Galleries of Verified Programs

- Visit our gallery of verified programs, as part of a larger gallery on the website of Toccata.
- A mini-gallery of verified sorting algorithms, by J.-J. Levy and C. Ran
- A gallery of verified programs involving floating-point arithmetic, by S. Boldo

### Lecture Notes

- Deductive Program Verification with Why3 (lecture at Digicosme Spring School 2013)
- (in French) Vérification déductive de programmes avec Why3 (JFLA, France, 2012)

### Other Student Lectures using Why3

- Course
*Proofs of Programs*at the*Master Parisien de Recherche en Informatique* - (in Portuguese) Courses
*Formal methods*and Certified Programming at the Universidade da Beira Interior, Portugal - (in french) course
*Méthodes formelles et développement de logiciels sûrs*at the*Master Informatique de l'Université de Rennes* - (in french) course sémantique des langages, third year of Supelec Engineering School

## Projects using Why3

- EasyCrypt: toolset for reasoning about relational properties of probabilistic computations with adversarial code
- Frama-C: extensible and collaborative platform dedicated to source-code analysis of C software; and its WP plug-in for deductive verification
- SPARK 2014: formal verification tool for Ada
- Krakatoa: verification tool for Java; and the Jessie plug-in of Frama-C, distributed as part of the former Why tool.
- BWare project: discharging proof obligations generated by Atelier B using multiple provers

### Some papers from users of Why3

- Formal Verification of Control Systems Properties with Theorem Proving Dejanira Araiza-Illan, Kerstin Eder, Arthur Richards
- Suppl : A Flexible Language for Policies Robert Dockins and Andrew Tolmach
- Verification and testing of mobile robot navigation algorithms: A case study in SPARK Piotr Trojanek and Kerstin Eder
- Automated algebraic analysis of structure-preserving signature schemes by Joeri de Ruiter
- Software product line for semantic specification of block libraries in dataflow languages by A. Dieumegard, A. Toom, M. Pantel.

## External Provers

This section gives a few tips to download, install and/or configure external provers. Each time a new prover is installed, you must rerun the command`why3 config --detect`. Using the latest version is recommended (except for Yices, see below) and the config tool above will tell you if the version detected is supported or not.

For beginners with Why3, we recommend to install Alt-Ergo, CVC3, and Z3. They are open-source, available for many architectures, and together provide a fairly efficient prover support.

For more advanced use, installing Coq is also good to discharge complex VCs, such as when induction is
required. It is also useful to understand why VCs are not proved,
that is to debug the input program or its specification. In case of
using Coq, we recommend to give a try to the `why3` Coq tactic.

### Automatic provers

**Alt-Ergo**- available under binary form for Unix and Windows, or under source form to be compiled using the OCaml compiler, from this page.
**Beagle**- a first-order theorem prover, available from this page
**CVC3**- available under source form and as a Linux binary from this page
**CVC4**- available under source form and as a Linux binary from this page
**E-prover**- available under source form as well as some binary format from this page
**Gappa**- a prover specialized on verification of numeric formulas, including floating-point numbers, available under source form from this page
**Metis**- a first-order theorem prover, available from this page
**Metitarski**- a prover specialized on verification of numeric formulas, available from this page
**Princess**- a first-order theorem prover supporting linear integer arithmetic, available from this page
**Simplify**- available under binary form for various architectures from this page or directly here
**SPASS**- available under source form as well as some binary format from this page
**Vampire**- available under binary form from this page
**veriT**- available under source form from this page
**Yices**- available under binary form for various platform from this page. Both Yices1 and Yices2 can be used.
**Z3**- available under source form from this page

### Interactive provers, a.k.a. Proof assistants

**The Coq proof assistant****The PVS specification and verification system****Isabelle/HOL**