Proving the Safety of Autonomous Systems with Formal Methods - What Can You Expect?

This contribution briefly recapitulates the notions of autonomous systems and formal methods and clarifies their meaning as used in the following. Two examples of possible fallacies with formal syntax and semantics are given, but irrespectively of that, a perfect formal method is assumed for the rest of the paper. In the main part three examples are given, where even with a perfect formal proof of certain safety aspects, safety may nevertheless be compromised. The reasons for this are environmental influence, unaccounted world knowledge, and misbehaviour of neighbour systems. As conclusion, however, the use of formal methods is not discouraged at all, but awareness of the limitations of formal methods is requested from everybody.