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
- 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