[p4bl0]

This is a very good outreach paper on formal methods. One important thing has to be taken into account and is not quite straightforward to get from the article. Formal methods work on formal models. It is possible to have very good formal models for safety (stating e.g., that the train doors must always be closed when the train is in motion), but it is very hard to come up with good formal model for security (e.g., no one should be able to open the door when the train is in motion). Because of the adversarial setting of security, it is not a good idea to assume that you covered everything in your model (does your model formalize that guy with a crowbar?). Vulnerabilities are often found outside of the specifications of a system. A great example of that is side-channel attacks on cryptography.