# Measuring verification performance

To see a more detailed breakdown of where Verus is spending time, you can pass
`--time` on the command line.  For even more details, try `--time-expanded`.
For a machine-readable output, add `--output-json`.  These flags will also
report on the SMT resources (rlimit) used.  SMT resources are an advanced topic;
they give a *very rough* estimate of how hard the SMT solver worked on the provided
query (or queries).

See `verus --help` for more information about these options.