The ever growing pervasiveness of software systems in modern days technology results in an increasing need of (software) program correctness proofs. The latter, allow developers to spot software failures before production, hence preventing potentially catastrophic repercussions on our society, as in the case of safety-critical infrastructures. Unfortunately, correctness proofs may fail, even when software is actually correct, due to program analysis imprecision, which pays the price of losing information for gaining decidability. In standard abstract interpretation-based static analyses, such imprecision is “measured” in terms of completeness of the chosen observation (i.e., of the abstract domain) w.r.t. the programming language semantics. In this setting, fixed the language to analyze, it is crucial to have decidable techniques to determine whether the chosen abstraction is precise enough for the program under analysis. In this paper, we explore abstract domain precision characterization from a novel point of view, providing a formal framework for characterizing and (statically) verifying abstract domain precision, that can be adopted also in the case of ``weakened'', Galois Connection-less, static analysis frameworks. Distinctive examples adopting such frameworks are the Convex Polyhedra and Automata domains, for which standard approaches to reason about analysis precision, referred as completeness, cannot be applied.