To run ES-Verify, select ``Run ES-Verify'' from the ``Tools'' menu.
ES-Verify tool runs as a separate thread inside ESpec tool. This process is CPU intensive and usually takes a long time. User should wait for the process to finish. A syntax error in the input Eiffel file or a translation error will stop the process automatically and the failure will be reported to the GUI. ES-Verify can also be stopped manually at any time by the user if the ``Stop'' button is pressed.
The result of running the theorem prover will be displayed inside ESpec main window. If all proof obligations are discharged successfully, the green bar will be shown. User can see the generated HTML proof file by double clicking on it (``output proof html path'').
When user chooses to see the generated HTML proof file, ESpec opens the generated file in the HTML viewer.
The failures (if any) are reported to the ESpec GUI. These errors can lead the developer to the location of the problem in the original Eiffel file.
User can request to see the un-proven rules by double clicking on the ``Output un-proven html path''.
The un-proven HTML will be opened in a new window. This output will help the expert developer (with PD knowledge) to fix the code.