All of mathematics formulated using ZFC can be "formalized" in the sense that each statement could be translated into a logical string, and each proof can be translated into a formal proof. This is never actually done, but it is important to know that it could be done in principle.
However, I have never seen a formal language or proof theory for the subjects of metalogic, proof theory, or model theory, whose statements "discuss" the provable statements of logical theories. For example, all the proofs of things like compactness theorems, (in)completeness theorems, etc., seem to be naive, in the sense that they use human language and intuitionist logic in order to psychologically convince the reader of a particular statement.
Does there exist a way to formalize the sentences and proofs of metalogic in the same way that logic itself is formalized? Is there a book that develops metalogic/proof theory/model theory along these lines? Or are these subjects "inherently" naive for some in-principle philosophical reason?
It seems that the issues discussed in this answer could be addressed nicely by such a formalism.