This project aims at independent verification of the code used in Thomas Hales' proof of the Kepler Conjecture and the Hales/McLaughlin proof of the Dodecahedral Conjecture.