Small proof checkers increase trust in the results of theorem provers by providing independent and trustworthy validation of results; even more, these checkers can be carefully architected to be reusable across proof formats and enable the communication and sharing between systems of proofs and their meaning. One such architecture is the FPC framework, based on sequent calculi for various logics, notably classical and intuitionistic. We describe purely functional implementations of determinate proof-checking kernels in OCaml and Gallina, and correctness of the latter is given by a formal proof of soundness in Coq, from which a verified checker can be extracted; we also discuss the integration of these tools in the context of general, not necessary determinate proof checking, and directly within proof assistants.