We describe the specification and proof of an (imperative, sequential) hash table implementation. The usual dictionary operations (insertion, lookup, and so on) are supported, as well as iteration via folds and iterators. The code is written in OCaml, translated to Coq by the CFML tool, and verified using higher-order separation logic, embedded in Coq.