[IsThisObvious]

I know people who write crypto software that must conform to formal verification of the algorithm, requires detailed design documentation before a single line of code, etc.

[z-factor]

Funny thing is that code is then compiled with a compiler was not formally verified, so it's still a 'fingers crossed' situation.

[IsThisObvious]

The code generator we use (at my job; not crypto) was written in Coq and formally verified to generate code with certain properties, given properties of the input.

I assume that the crypto group I know, who developed most of the code generator I use, takes similar measures to make sure that their verified "theorems" translate correctly to code.

The unverified stage is actually the hardware, which is an open problem.

[jdiez17]

Right, but it's much less of a leap of faith, IMHO. Besides, if you turn off optimisations you can be reasonably sure the compiler didn't do something unintended.

[foobarqux]

I meant volunteer to mean "not get paid".