Special Portal URLs
When you run the Certora CLI, the tool outputs a link to the generated verification report. By modifying this link, you can access additional files that the tool generates. These are primarily intended for the tool developers, but they can also be helpful for users in some cases. This page lists these outputs and explains how to read them.
The job status page contains information about the job, including the arguments that were passed to the command line, the job message, and the exact Certora Prover version. It is created as soon as the job is submitted, and also shows the current status (whether the job has started or finished processing).
To access the job status page, change the
output component of the URL to
jobStatus. For example,
Additional error reports
The Certora team is actively working to improve the generated reports; we expect
that in the near future,
Results.txt will be
FinalResults.html is an older version of the verification report, but
occasionally contains more information than the newer report format, especially
in cases where the tool encountered an internal error. In certain cases, it
may be generated even when the main verification report is not.
If the main verification report shows an error and you want to find more
information, try checking
FinalResults.html. To access it, add
Just before the
? in the URL. For example,
Another potential source of information is the file
captures the command line output of the tool. It can be accessed by putting
Results.txt before the
The Certora Prover performs several different kinds of bytecode analysis to improve the running time of verifications. Occasionally, some of these analyses fail, which can sometimes cause timeouts.
statsdata.json file contains a section called
ANALYSIS that lists all
of the analyses that are attempted, and whether they succeed or fail. If you
see that a particular method consistently causes timeouts, you can check the
ANALYSIS section to see if that method was correctly analyzed. The analysis
section should have a
true for each successful analysis, and a
each unsuccessful analysis.
statsdata.json indicates an analysis failure on a method that is
consistently timing out, we encourage you to
contact Certora Support; our developers may be able
to help resolve the issue.
For example, the following shows that the
POINTSTO analysis is failing on
createMarket method, which may cause verification of rules involving
createMarket to take a long time:
Some analysis failures are expected. In particular, analysis failures on constructors and the fallback method are expected and typically do not lead to problems.
These analyses only depend on the bytecode being verified (not the rules), so you should only need to recheck them if your contracts changes.
To access the
statsdata.json file, add
statsdata.json before the
? in the
When a job is submitted, all of the input and output are stored. You can
retrieve these files by replacing
zipOutput in the URL:
This link will allow you to download a tar file. The submitted specs are
contained in the
TarName directory, and the original contracts can be found
TarName/input/.certora_config directory (the file names will be
The zip output cannot be downloaded unless you have logged in to the portal with an appropriately authorized key. If you receive a “Forbidden” error message, log in to the main Certora Portal page with your Certora key.