  We present a new abstract interpretation framework for the precise
over-approximation of numerical fixpoint iterators. Our key observation is that
unlike in standard abstract interpretation (AI), typically used to
over-approximate all reachable program states, in this setting, one only needs
to abstract the concrete fixpoints, i.e., the final program states. Our
framework targets numerical fixpoint iterators with convergence and uniqueness
guarantees in the concrete and is based on two major technical contributions:
(i) theoretical insights which allow us to compute sound and precise fixpoint
abstractions without using joins, and (ii) a new abstract domain, CH-Zonotope,
which admits efficient propagation and inclusion checks while retaining high
precision. We implement our framework in a tool called CRAFT and evaluate it on
a novel fixpoint-based neural network architecture (monDEQ) that is
particularly challenging to verify. Our extensive evaluation demonstrates that
CRAFT exceeds the state-of-the-art performance in terms of speed (two orders of
magnitude), scalability (one order of magnitude), and precision (25% higher
certified accuracies).
