---
name: "why"
section: "1"
platform: "linux"
package: "why"
version: "2.34-2"
release: "Debian 8 (Jessie)"
platforms: ["linux"]
url: "https://new.carta.tech/why"
---

# why(1)

A multi-language multi-prover verification tool

## NAME

why - A multi-language multi-prover verification tool

## SYNOPSIS

**why** \[ **options** \] **files**

## DESCRIPTION

**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).

## OPTIONS

- **-h**

  Help. Will give you the full list of command line options.

## AUTHORS

*Jean-Christophe Filliatre \<filliatr@lri.fr\>*

## SEE ALSO

*Why web site: http://why.lri.fr/*