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

▲

amelius 5 hours ago | parent [-]

And you can put the specification in the manual of the software so the user knows what they're dealing with.

▲

heikkilevanto 5 hours ago | parent [-]

But can you make a mere user read and understand that specification?

	▲	amelius 5 hours ago \| parent [-]
		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.