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||check verification conditions in source code|
|why3bench||schedule verification checking|
|why3config||detect provers usable by why3|
|why3-cpulimit||run a command with CPU and virtual memory limits|
|why3doc||format Why3 theories in HTML|
|why3ide||start the Why3 IDE|
|why3ml||generate verification conditions from Why3ML programs|
|why3realize||produce a realization of a Why3 theory|
|why3replayer||execute the proofs in a Why3 session file|