Must Program Verification Systems and Calculi be Verified?
Bernhard Beckert, Vladimir Klebanov
With this paper, we want to provoke discussion on whether verification
tools and calculi themselves need to be formally verified. We argue
that though verifying the verifier is useful, it is not an absolute
necessity. The (limited) resources in academia may be better spent on
improving verification systems in other ways.