Deductive verification offers the strongest guarantees for demonstratating that software is bug free. For software such as realistic abstract interpreters, the verification requires interaction with a proof assistant. This lecture will explain how deductive verification can be applied to software used to produce software, and notably static analyzers and compilers. It will present some research projects where the Rocq proof assistant was used to verify an abstract interpreter for C inspired by Astrée. Last, the lecture will discuss the advantages of this approach for developing critical embedded software, particularly the fact that the guarantees provided by abstract interpretation carry over to the compiled code.