upvote
Depends which way you mean. It is possible to provide a formal specification for a proof verification engine and prove, in the same language that the engine is for, that the engine implements that specification.

Proving that the system it implements is like, logically sound, is a different issue, and for that you do need stronger axioms.

reply