Package why3

Software verification platform

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.

Version: 1.4.0

General Commands

why3 check verification conditions in source code
why3-cpulimit run a command with CPU and virtual memory limits
why3bench schedule verification checking
why3config detect provers usable by why3
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