This talk outlines the ingredients that go into producing a formally verified proof of Mactinyre's Quantified Elimination theorem for the p-adic numbers using the Isabelle/HOL proof assistant. Given that every mathematical technique used in a formal proof must itself be formally verified, careful thought needs to be put into the proof strategy, and significant work is required to build the foundational lemmas and definitions within the constraints of the Isabelle language and existing proof libraries. We'll discuss some of the specific challenges posed by the choice of formal framework and give an outline of the structure of the formal proof.