Prover version 7.3.0
is out! This update aims to enhance your user experience and address some minor bugs reported by our users.
New Web Features
Jump to Spec
Quickly locate rule definitions or assertion messages within your spec file by clicking the new icon in the Rules
, Rule Call Resolution
, or Global Call Resolution
tab items.
Real-time insights
Stay informed with the new Live Statistics tab, providing key metrics on path count, non-linear operations, and memory/storage complexity before job completion. These metrics guide simplification strategies to optimize Prover performance.
Job configurations tab
Explore the new Configuration tab to quickly access the exact settings used for your verification job
Prover Updates
- Easy access to immutables
Accessimmutable
variables directly, even if they are private. Read more | Example - Advanced rule selection
Enhance filtering flexibility with wildcard (*) support in--rule
or utilize--exclude_rule
for seamless exclusion. Read more - Reason about
blobhash
Verify advanced specifications with Prover's new support for blobhash instruction and hooks. Read more - Preliminary support of
transient storage
Preliminary support fortload
andtstore
operations in inline-assembly Solidity, along withALL_TLOAD
andALL_TSTORE
hooks. Read more | Example - Dispatch-list summarization
Enhance contract behavior modeling with dispatch-list summarization, enabling precise representation of smart contract actions for statically unresolved calls. Read more | Example - Precise bitwise operations
Fine-tune modeling by using--precise_bitwise_ops
to model bitwise operations precisely with the tradeoff of lowering mathint accuracy. Read more | Example - Local compilation checks
Speed up development with--compilation_steps_only
, enabling local compilation and syntax validation of spec files without server connection. Read more
Access these updates by ensuring your software is up-to-date with the latest version. To upgrade to v7.3.0, simply run pip install --upgrade certora-cli
.