A formal proof is a proof in which every single logical inference has been checked all the way back to the fundamental axioms of mathematics. Because of the large number of logical steps involved, formal proofs are generally carried out by computer. This talk will describe the general technology involved in formal proofs and will highlight some of the latest developments in this area. This talk will discuss an ongoing project called "Flyspeck" that aims to give a complete formal verification of the Kepler conjecture. (The Kepler conjecture asserts that the familiar cannonball arrangement of congruent balls gives the highest possible density.)