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.
(See the specific section below for the list of supported
provers.)
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. (See Projects using Why3 below.)
Why3 can be easily extended with support for new theorem provers.
Why3 can be used as a software library, through an OCaml API.

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

## Documentation and Examples

### Related Publications

### Examples, Galleries of Verified Programs

### Lecture Notes

### Other Student Lectures using Why3

*(Do not hesitate to contact us if you use Why3 for teaching, we would be happy to add a link to your course's page here)*## Projects using Why3

*(Contact us if you want your project listed here)*- 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. See also the ProofInUse project
- 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
- CAPS: A Calculational Assistant for Programming from Specifications
- AstraVer project for deductive verification of Linux kernel code
- Formal Verification for Solidity Contracts
- Formal Combinatorics: Formally specified and verified enumeration programs

### Some papers from users of Why3

*(Contact us if you would like your paper to be listed here)*- 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.
- Rodin Platform Why3 Plug-In by Alexei Iliasov, Paulius Stankaitis, David Adjepon-Yamoah, Alexander Romanovsky
- Automated Verification of Functional Correctness of Race-Free GPU Programs by Kensuke Kojima, Akifumi Imanishi1, Atsushi Igarashi
- (in French) Preuve de programmes d'énumération avec Why3 by Alain Giorgetti, Rémi Lazarini

## 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, CVC4, and Z3. They are free software, available for many architectures, and all together provide a fairly efficient prover support.

For more advanced use, installing Coq is also good to discharge complex VCs. 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**- an SMT-based theorem prover supporting quantifiers, polymorphic sorts, and various theories including equality, linear and non-linear arithmetic over integers or rational numbers, arrays, records, ennumerated types ; available from this page.
**Beagle**- a theorem prover for first-order logic with equality over linear integer/rational/real arithmetic ; available from this page
**CVC3**- an SMT-based theorem prover ; available from this page
**CVC4**- an SMT solver supporting quantifiers and many theories including equality, arithmetic, datatypes, bitvectors ; available from this page
**E prover**- a theorem prover for first-order logic with equality ; available from this page
**Gappa**- a solver specialized on the verification of numeric formulas, including floating-point numbers ; available from this page
**Metis**- a theorem prover for first order logic with equality ; available from this page
**Metitarski**- a prover specialized on verification of numeric formulas ; available from this page
**Princess**- a prover for first-order logic modulo linear integer arithmetic ; available from this page
**Psyche**- a modular platform for automated or interactive theorem proving ; available from this page
**Simplify**- an automatic SMT-based prover available under binary form for various architectures from this page or directly here
**SPASS**- a theorem prover for first-order logic with equality ; available from this page
**Vampire**- a theorem prover for first-order logic with equality ; available from this page
**veriT**- an SMT-based theorem prover supporting quantifiers, equality, linear arithmetic over integers or rational numbers ; available from this page
**Yices**- an SMT solver supporting equality, linear real and integer arithmetic, bitvectors, scalar types, and tuples ; available from this page. Both Yices1 and Yices2 can be used, although Yices2 do not support quantifiers.
**Z3**- an SMT solver supporting quantifiers and many theories including equality, arithmetic, datatypes, bitvectors ; available from this page