I did a little of this stuff many years ago, mainly for software verification. The surprising thing is that many errors are caught during the process of preparing the material for verification, and almost none are caught during verification. This latter arises either because the specification is wrong in some respect (e.g., doesn't capture the concept precisely) or because the verification system is faulty, or because there aren't any errors left (hah!). At the time, there seemed to be general agreement that the process of specifying and verifying things (theorems, software, hardware) was valuable, but it was also extremely expensive and required a new class of experts. Automated theorem verification could become a new mathematical specialty, generating its own kind of complexity theorems and great unsolved problems. Hilarie