Okay, here is my attack:<p><pre><code> 1. Find drone operators home addresses, information whether they have significant others, kids. Most of this is public or fairly low security information.
2. Send goon squad to pick up significant other and kids
3. Send threatening message with proof you have significant other and kids with the correct level of pressure for drone operator to follow your instructions very carefully.
4. Now disappear. Very quickly, yeah, the military doesn't like to demonstrate that it has glaring weaknesses in their security and tend to send goon squads the other way to solve the issue.
</code></pre>
That said, ultimately I proposed a social engineering attack, there are quieter less threatening methods available that could be effective with enough planning. Ultimately the point here is, formal verification can't work, for it to work the model it is verified against must include every possible form of outside influence and the code at all levels must be 100% verified against that model.<p>So you need to verify everything (including the workstation doing the verification against absolutely every possibility) this is an exponentially hard problem. This is why formal verification is used only in small areas, and why it does not always work, please see the 1990 Arianne 4 launch failure, where while most of the avionics had been formally verified certain data tests had been removed for optimisation and when a sensor fed bad data meant the computer had a bad cast to different data type ditching important information.