even if software is formally verified, and even assuming the specification is both totally accurate and complete, there is plenty of room for issues at software deployment in a multi-component system such as this