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