I originally shared this just under two years ago, but I want to resubmit it again. Why? Because in the time since the last submission, we went from seven proofs of leftpad to 17! You can now compare Agda’s proof style to ACL2, see how to formally prove Java correct, and even read a proof for an FPGA process! People are, of course, welcome to submit proofs for languages not yet present.

        Comments