We present a technique for generating proof certificates in the model checker Kind 2 as an alternate path of qualification with respect to DO-178C. We developed a version of Kind 2 that generates proof certificates, allowing to shift the trust from the model checker to the proof checker (LFSC). Certificates for the actual model checking algorithm are generated as SMT2 files and verified by an external SMT solver. The translation from Lustre to the internal first-order logic representation is verified in a lightweight way by proving observational equivalence between independent frontends (here JKind and Kind 2). This proof is actually carried by Kind 2 itself and generates in turn its own proof certificates.