The most common proofs are those that the compiler constructs while type checking. The compiled program is the proof witness. All compilers can be thought of as producing a proof-by-construction but they vary wildly in the propositions they can prove.

If this idea is new to you and you want to learn more, google "propositions as types" or "the curry howard correspondance".