Proofs are programs.
Formal verification of programs is a huge research area. (See, for example, the group at Carnegie Mellon.)
Many complex programs have been verified; for example, see this kernel written in Haskell (repaired 404 link is for seL4, see also the moved to location and the project’s website).