  Formally verified compilers and formally verified static analyzers are a
solution to the problem that certain industries face when they have to
demonstrate to authorities that the object code they run truly corresponds to
its source code and that it satisfies certain properties. From a scientific and
technological point of view, they are a challenge: not only a number of
nontrivial invariants and algorithms must be proved to be correct, but also the
implementation must be reasonably effective so that the tools operate within
reasonable time. Many optimizations in compilers rely on static analysis, and
thus a formally verified compiler entails formally verified static analyses.In
this article, we explain some difficulties, possible solutions, design choices
and trade-offs pertaining to verified static analysis, in particular when the
solution of the analysis is expressed as some form of tree, map or set.
