SYNOPSISwhy [ options ] files
why is a verification tool. It takes annotated programs as input (in ML or C syntax) and outputs verification conditions for several proof assistants (Coq, PVS, HOL Light, Mizar) and decision procedures (haRVey, Simplify).
Help. Will give you the full list of command line options.
AUTHORSJean-Christophe Filliatre <[email protected]>