  We present the first formal verification of approximation algorithms for
NP-complete optimization problems: vertex cover, independent set, set cover,
load balancing, and bin packing. We uncover incompletenesses in existing proofs
and improve the approximation ratio in one case.
