Easy! Write a program that does a brute force check of Goldbach's conjecture on all integers. For each integer that passes the check, print a line. If you can prove this correct (or incorrect) you'll probably win a Fields medal.

I agree with the general point that you could prove such a simple program correct relatively easily but that does still have a cost, which is always a concern in an open-source project. You still need someone to step up and do that work and continue to verify it periodically in the future – if that code is doing complicated things with buffering, that opens up possible odd bugs due to stdlib, gcc, maybe even kernel behaviour changes which might not affect simpler programs.

Not a huge bit of work to be sure but for a non-commercial project you might have trouble finding a volunteer who cares about that tedium.

Absolutely, I once trivially proved a 1000,000 line implementation of return 0 to be correct. I don't know why all comments are bothered by how much overkill this yes implementation is. Maybe they don't hold 100,000 PhDs like we do, am I right?