Many Of The Benefits Of Formally Verifying Smart Contracts With Much Less Pain

3 min readFeb 7, 2019

Formally verifying smart contracts is extremely difficult. Fortunately, there is a subset that gives many of the benefits with vastly less effort. I refer to this as design debugging.

Design Debugging

Formal verification requires first defining what correctness means. Intentions (designs) must themselves first be unambiguously specified and verified. Intentions may be obvious for trivial programs, but, they can quickly grow in complexity for more elaborate code.

Few people realize that just debugging designs is exceptionally beneficial and yet much easier. It can catch deep bugs that will likely not be found even with extensive unit testing and auditing. Design debugging by itself may catch most, if not all, bugs that code verification would find!

Evidence

There is strong evidence that design debugging is practical and rewarding. For example, TLA+ is a design debugging tool Amazon used to discover bugs in S3 (Simple Storage Service) and EBS (Elastic Block Store):

"So far we have used TLA+ on 10 large complex real-world systems. In every case TLA+ has added significant value, either finding subtle bugs that we are sure we would not have found by other means, or giving us enough understanding and confidence to make aggressive performance optimizations without sacrificing correctness. We now have 7 teams using TLA+, with encouragement from senior management and technical leadership. Engineers from entry level to Principal have been able to learn TLA+ from scratch and get useful results in 2 to 3 weeks, in some cases just in their personal time on weekends and evenings, and without help or training."¹

Microsoft used TLA+ based design debugging to uncover a critical bug in the XBox 360:

“Writing a TLA+ spec caught a bug that would not otherwise have been found.”²

Intel as well as many other organizations have also enthusiatically embraced TLA+ based design debugging.

Criticism

A criticism of just design debugging is that there is no guarantee the corresponding implementations will be correct. Code verification unfortunately remains elusive for most projects. However, today design debugging advances software beyond what is possible with unit testing and auditing. While the lack of code verification cannot be discounted, the successes of design debugging cannot be dismissed either.