Why3 is the next generation of the Why software verification platform.
Why3 clearly separates the purely logical specification part from
generation of verification conditions for programs. It features a rich
library of proof task transformations that can be chained to produce a
suitable input for a large set of theorem provers, including SMT
solvers, TPTP provers, as well as interactive proof assistants.
why3 Verify conditions in source code. If the filename is "-", then input is read from stdin. why3bench The why3bench tool adds a scheduler on top of the Why3 library. It is designed to compare various components of automatic proofs: automatic provers... why3config Why3 must be configured to access external provers. Typically, this is done by either running this tool or using the menu File/Detect provers of the IDE. This... why3-cpulimit Run a command with CPU and virtual memory limits. One of -h or -s must be specified. TIME specifies the maximum runtime in seconds. MEMORY specifies the maximum... why3doc Format Why3 theories in HTML for human viewing. why3ide Start the Why3 IDE, either loading an initial file, or starting in a given project directory. why3ml This tool is an additional layer on top of the Why3 library for generating verification conditions from Why3ML programs. It accepts the same command line... why3replayer The purpose of the why3replayer tool is to execute the proofs stored in a Why3 session file, such as the one produced by the IDE. Its main goal is to play...