  Different theorem provers tend to produce proof objects in different formats
and this is especially the case for modal logics, where several deductive
formalisms (and provers based on them) have been presented. This work falls
within the general project of establishing a common specification language in
order to certify proofs given in a wide range of deductive formalisms. In
particular, by using a translation from the modal language into a first-order
polarized language and a checker whose small kernel is based on a classical
focused sequent calculus, we are able to certify modal proofs given in labeled
sequent calculi, prefixed tableaux and free-variable prefixed tableaux. We
describe the general method for the logic K, present its implementation in a
prolog-like language, provide some examples and discuss how to extend the
approach to other normal modal logics
