  Abstract interpreters are complex pieces of software: even if the abstract
interpretation theory and companion algorithms are well understood, their
implementations are subject to bugs, that might question the soundness of their
computations.
  While some formally verified abstract interpreters have been written in the
past, writing and understanding them requires expertise in the use of proof
assistants, and requires a non-trivial amount of interactive proofs.
  This paper presents a formally verified abstract interpreter fully programmed
and proved correct in the F* verified programming environment. Thanks to F*
refinement types and SMT prover capabilities we demonstrate a substantial
saving in proof effort compared to previous works based on interactive proof
assistants.
  Almost all the code of our implementation, proofs included, written in a
functional style, are presented directly in the paper.
