Why3 Logo

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. (See the list of supported provers below.) 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.

Try Why3 in your browser

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

Contact

Distributions

Sources Download

Main developers

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)

Some papers from users of Why3

(Contact us if you would like your paper to be listed here)

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.

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, enumerated 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
Colibri
an SMT solver based on ideas of constraint logic programming. Supports quantifiers and theories including equality, arithmetic, bitvectors, floating-point numbers; available from this page
CVC4
an SMT solver supporting quantifiers and many theories including equality, arithmetic, datatypes, bitvectors; available from this page
cvc5
an SMT solver supporting quantifiers and many theories including equality, arithmetic, datatypes, bitvectors; available from this page
dReal
a solver dedicated to formulas on real arithmetic; 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
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

Interactive provers, a.k.a. Proof assistants

Coq
a proof assistant in intuitionistic logic based on the calculus of inductive constructions; available from this page
PVS
a specification and verification system; available from this page
Isabelle/HOL
a proof assistant in higher-order logic; available from this page

INRIA Saclay - Île-de-France              Université Paris-Saclay              CNRS              LMF