Checking Specifications

Formal verification is only as good as the specification. If a specification has an error, it may fail to catch an important bug.

Certora has developed several tools to help catch errors in the specifications themselves. This chapter explains how to use these tools.

Todo

This chapter is incomplete. The following resources may be helpful:

• Certora’s Devcon 2022 presentation “Bad Proofs in Formal Verification”

• The --rule_sanity documentation