  Interval arithmetic libraries provide the four elementary arithmetic
operators for operand intervals bounded by floating-point numbers. Actual
implementations need to make a large case analysis that considers, e.g.,
magnitude relations between all pairs of argument bounds, positional relations
between the arguments and zero, and handling of the special values, infinities
and NaN. Their correctness is not obvious as they are implemented by human
hands, which comes to be critical for the reliability. This work provides a
mechanically-verified interval arithmetic library. For this purpose, we utilize
the Why3 platform equipped with a specification language for annotated programs
and back-end theorem provers. We conduct several proof tasks for each of three
properties of the target code: validity, soundness, and tightness; zero
division exception handling is also verified for the division code. To
accomplish the proof, we propose several techniques for
specification/verification. First, we specify additional lemmas that support
deductions made by back-end SMT solvers, which enable to discharge proof
obligations in floating-point arithmetic containing nonlinear terms. Second, we
examine the annotation of tightness, which requires to assume that a
computation may result in NaN; we propose specific extremum operators for this
purpose. In the experiments, applying the techniques in conjunction with the
Alt-Ergo SMT solver and the Coq proof assistant proved the entire code.
