Comment by mbrodersen

That makes me think that formally proving the code correct using a proof assistant would actually be faster than the process you describe.