There are a couple of branches worth mentioning in the "meta-proof". One is the proof of correctness of the proof-checking software. I believe that fiddlemath is addressing this problem. The "specification" of the proof-checking software is essentially a presentation of an "inference system". The second is the proof of the soundness of the inference system with respect to the programming language and specification language. In principle, this is a task which is done once - when the languages are defined. The difficulty of this task is (AFAIK) roughly like that of a proof of cut-elimination - that is O(n^2) where n is the number of productions in the language grammars.