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.
| Command | Description |
|---|---|
| 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 |