Nice mathematical theories deserve machine-assisted proofs. Trustworthy static analyzers deserve to be formally verified. These are two good reasons to try to mechanize the theory of abstract interpretation and its applications using proof assistants. This talk will report on several attempts to formalize abstract interpretation with the Coq proof assistant, based mainly on David Pichardie’s PhD work and our collective work on the Verasco verified static analyzer, and compare them with the work of Nipkow and of Darais and Van Horn, using other proof assistants. While proving the soundness of a static analyzer based on abstract interpretation works very well, parts of the classic presentation of abstract interpretation can be a challenge for a system such as Coq. I will discuss some of these issues and whether they are due to limitations of Coq not present in other logical systems.