ES-Verify component of ESpec, translates the input Eiffel files (which are specified in the test suite) to the Perfect Developer language and then runs the Perfect Developer theorem prover on the translated files. For settings, press the ``Settings'' button under ``ES-Verify'' button in the main window. This opens the ``ES-Verify settings'' window. User must select the project executable located in EIFGENs folder.