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.


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