Since the automatic theorem prover Vampire uses a variety of techniques to find proofs, it is a complex piece of software with a large trusted code base. To enhance trust in the the proofs Vampire produces, they could be checked with an interactive theorem prover with a small kernel and thus a much smaller trusted part. We report on work in progress to verify Vampire proofs in $\lambda \Pi$-calculus Modulo Theories, the underlying type theory of Dedukti.