Let us continue with this example of the flawed proof engine, and consider a recovery scenario. Suppose that further study and improvement of the inference engine leads to the judgement that there is an easy bug fix, and that there is a simple test that detects at least the bad inferences that the older version of the engine erroneously okayed. Now we have fallen into doubt about already certified proofs. One simple fix is to employ a similar form of certificate, the difference being that it invokes the new engine rather than the old one, and simply try to certify all the old inferences with the new form of certificate. The old certificates need not be deleted, although perhaps they may be eventually.
Consider now a more sophisticated scenario. Stipulate a form of certificate that is created this way: given an inference step, first look and see if there is a certification for it (pointing to it) of the old sort that uses the defective engine; if there is no old-engine certificate then use the new engine; if there is an old-engine certificate then apply the test for possibly-bad inferences postulated above for this scenario; if the inference is possibly-bad then use the new engine, but otherwise, simply point to the old-engine certificate. If there were many proofs with the old engine but the bulk of inferences were okay according to the new test, and if running the engine is often expensive, then this method could represent a significant efficiency as a corrective.
Let's do a quick survey of when these various certificates are appropriate. Let's also make the more interesting assumption that whether the engine is flawed is not agreed upon by all parties. Persons who think the old engine was correct will still accept the old certificates with their original significance for correctness. Persons who think the new engine is correct and that the test for possibly-bad cases is an accurate assessment will accept both new-engine certificates and also the hybrid certificates that depend on the old engine. Persons who think the new engine is correct but don't trust the test for possibly-bad cases will insist on the simple new-engine certificates. All these certifications can coexist, even if their external significances are in dispute.
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html