The guarantees of formally verified systems are only as strong as their trusted specifications. As observed by previous studies, bugs in formal specifications could invalidate the assurances that proofs provide. These types of specification bugs are difficult to debug and have been found to exist in practice.

Beyond manual inspection, there is currently no structured way to gain confidence that a specification is correct. Due to the trusted role specifications take, it would be impossible to prove a specification correct. We take a compromised approach, of testing specifications to help increase trust in specification correctness; who watches the watchers?

In this paper, we propose automatic and manual techniques to enable the ability to test specifications in Dafny. Drawing inspiration from classical software testing practices we introduce IronSpec, a framework for testing specifications. IronSpec enables automatic specification mutation testing to identify cases of specification weakness. This automation is complemented by a unit testing methodology for writing Spec-Testing Proofs (STPs) for a given specification. We evaluate IronSpec on nine specifications, including three specifications of open-source verified systems. Our initial results show that IronSpec is effective at flagging discrepancies between the original specification and the intent of the test writer, and has led to the discovery of specification bugs in each of the three open-source verified systems.