What do Formal Methods actually Guarantee?

A revised version of this article was published at https://medium.com/alacris/what-do-formal-methods-actually-guarantee-d94ae8802be2

There is a lot of misunderstanding about what formal methods can do — their powers — and what they cannot do — their limitations. Those who are mistaken about one side of the argument, exaggerating it or downplaying the other, or are simply too aware of one side yet insufficiently aware of the other, may end up being overly skeptical of formal methods or overly enthusiastic about them. In this short essay I’ll try to make both cases clear, and thus explain the value proposition of formal methods without falling into easily rejected claims.

Limitation: Formal methods are not a magic powder that you can sprinkle over your code to make it correct.
Power: Formal methods are a structural backbone around which you can develop more robust code.

Limitation: Formal methods are only methods. To have useful results at all, you still need to apply them, correctly, to the right problems.
Power: When applied correctly, formal methods can eliminate not only single actual bugs, but entire classes of potential bugs and attacks, that your model can express are absent.

Limitation: Formal methods won’t prevent bugs on aspects of your code that you haven’t formalized (yet).
Power: Formal methods can ensure the non regression of your code with respect to those classes of defects you have formalized. Unlike other methods, they provide a ratchet that ensures progress even as the code evolves.

Limitation: Formal methods can’t eliminate bugs and prevent attacks that go below the model you use (e.g. SPECTRE attack).
Power: Formal methods allow you to reason at one high level of abstraction and transport your results to a lower level of abstraction, provided you also prove full abstraction.

Limitation: Formal methods cannot be used to prove “everything” correct. There are always more things you could reason about.
Power: While there are infinite further issues, previous issues are finite and those that can be solved can be fully solved with finite effort.

Limitation: Formal methods suppose your domain is well-defined and limited enough to be specifiable, and that you actually understand it enough to specify it.
Power: Formal methods are a discipline that when to stick to them, will naturally lead you to your understanding your domain better.

Limitation: Formal methods cost a lot in terms of time and talent. They cost even more as you explore new spaces that require reasoning infrastructure.
Power: In many applications where millions of dollars worth of assets, or even lives, are at stake, it can be even more expensive not to use formal methods.

Limitation: Not everyone can use formal methods.
Power: A large fraction of developers can be trained to use formal methods. As for those who really can’t, they are probably a liability when it comes to safety-critical code.

Limitation: Formal methods can only prove formal guarantees, and only based on a lot of formal assumptions (axioms). And they cannot establish the informal guarantees that matter to humans.
Power: Formal methods help you make explicit what your assumptions and your guarantees are and ruthlessly eliminate any flaw between the assumptions and guarantees.

Limitation: Formal methods won’t save you from having to make a lot of assumptions about the vast amount of software and hardware that you depend on under your system.
Power: Formal methods will prevent the multiplication of implicit assumptions you don’t know about, don’t track, and don’t check as your system evolves, that may once have been true yet will cause catastrophic errors when they stop being valid (see Ariane V).

Limitation: Just because it’s true doesn’t mean it’s provable. There are correct programs that formal methods can’t prove correct.
Power: You shouldn’t deploy an program in a setting where safety matters unless you at least have an informal proof of safety. Then, making that informal proof formal is not only possible, but doable and useful. Formal methods are not magic, but neither are informal methods.

Limitation: Even for the things you can prove, often you can’t afford to prove them.
Power: You can use formal methods strategically: study what kind of serious or catastrophic issues similar projects have had that are worth eliminating, and build your model accordingly.

Limitation: Formal methods can’t prove the correctness of a system that isn’t correct to begin with.
Power: Formal methods help you identify flaws in your reasoning, find bugs and attacks you hadn’t thought of, abandon false solutions and pursue actual solutions.

We at Legicash believe that software professionals and executives tend to vastly underestimate the value of formal methods — that, as the name indicates, are not mere products you can use but processes you can enact. This is especially true in the domain of cryptocurrency dApps, where contracts can’t be fixed after they are launched: a lot of people have lost up to hundreds of millions of dollars belonging to themselves or to their customers due to software bugs that a modicum of formal methods could have caught — if not necessarily the first time around, at least the subsequent times.

Happily, there is a small but growing number of serious projects to improve smart contracts using formal methods, some of which have already borne valuable fruits. However, we at Legicash think that the existing efforts though useful remain desperately low-level with respect to the problem of building dApps. That is why we are working on providing better solutions that will help build the massively scaled dApps of tomorrow — and not just their smart contracts — in a way that is correct by construction. But this will be a topic for future articles.

Until we publish our next article, we invite you to share your thoughts and continue the conversation on Telegram at https://t.me/LegicashCommunity.