Comment by Almondsetat
5 hours ago
Everyone knows that the weak link is the specification. But this is a spurious argument, since, by definition, if you guarantee the implementation the only thing that's left exposed is the spec itself. At least you're reducing the attack surface
And you can put the specification in the manual of the software so the user knows what they're dealing with.
But can you make a mere user read and understand that specification?
Not all users are the same and that's OK. Just like not everybody needs to read and verify the Linux kernel.
Also note that a specification can be input to other tools, such as a formal verification system for an encompassing system.