EVES

As of June 2005, ORA Canada can no longer distribute EVES.

EVES is a state-of-the-art formal methods tool, developed by ORA Canada, that incorporates a unique set of technologies:

• a single language, called Verdi. Verdi is a formal notation, based on a version of untyped set theory, that can be used to express rigorous mathematical concepts, and thus provides an alternative to higher-order languages. Verdi supports large scale abstraction and information hiding through an Ada-like library mechanism.
• a proof obligation generator. The proof obligation generator automatically emits the assertions that must be proven to demonstrate certain important properties, including that code is in consonance with their specifications.
• an automated deduction system, called NEVER. NEVER is the automated deduction component of EVES. It is an interactive theorem prover that is capable of automatically performing large proof steps, yet can be finely directed by the user. Its design was initially influenced by the Bledsoe-Bruell prover, the Stanford Pascal Verifier, the Boyer-Moore theorem prover, and the Affirm theorem prover.
  NEVER is neither a fully automatic nor an entirely manual theorem prover. Although NEVER provides powerful deductive techniques for the automatic proof of theorems, it also includes simple user steps which permit its use as a system more akin to a proof checker than a theorem prover. The possible fine control of the prover allows users to closely investigate proof strategies and determine why, for example, proofs are failing. In our view, the synergism of powerful automated support and user control is a necessary precondition to a successful general purpose theorem prover.
• an interpreter.
• a compiler. The most recent compiler for the EVES system is the SPARC Verdi compiler. The development of this compiler was more "rigorous" than most: there are formal specifications for each pass of the compiler, and a proof that the semantics of a Verdi program (for a subset of Verdi) are "congruent" with those of the generated intermediate language.

Particular effort has been directed at the mathematical foundations of EVES. Consequently, Verdi was developed with a denotational semantics and the proof obligations were justified mathematically. In addition, the compiler was rigorously developed; that is, the machine-independent parts of the compiler have been justified mathematically. While NEVER is too complex (due to the combination of heuristics and non-axiomatic decision procedures) to be justified mathematically, a tool has been developed for checking NEVER proofs for correctness. The proof checking tool is a small program and is amenable to mathematical justification.