  Good tools can bring mechanical verification to programs written in
mainstream functional languages. We use hs-to-coq to translate significant
portions of Haskell's containers library into Coq, and verify it against
specifications that we derive from a variety of sources including type class
laws, the library's test suite, and interfaces from Coq's standard library. Our
work shows that it is feasible to verify mature, widely-used, highly optimized,
and unmodified Haskell code. We also learn more about the theory of
weight-balanced trees, extend hs-to-coq to handle partiality, and -- since we
found no bugs -- attest to the superb quality of well-tested functional code.
