Another usage of formal verification to great, claimed, benefit in the realm of distributed systems. I am yet to see anyone in finance using any formal verification techniques.
Design reviews, code audits, stress testing, and fault injection are all invaluable tools we use regularly, and always will. However, we’ve found that we need to supplement these techniques in order to confirm correctness in many cases. Subtle bugs can still escape detection, particularly in large-scale, fault-tolerant architectures. And some issues might even be rooted in the original system design, rather than implementation flaws. As our services have grown in scale and complexity, we’ve had to supplement traditional testing approaches with more powerful techniques based on math and logic. This is where the branch of artificial intelligence (AI) called automated reasoning comes into play.
Their use of automated reasoning focuses on code correctness and maintainability rather than performance optimization. While I initially expected it might automatically identify efficiency improvements, its primary value lies in making the codebase more robust and adaptable to changes.
The reason is that the bug fixes we make during the process of formal verification often positively impact the code’s runtime. Automated reasoning also gives our builders confidence to explore additional optimizations that improve system performance even further. We’ve found that formally verified code is easier to update, modify, and operate, leading to fewer late-night log analysis and debugging sessions.
One other challenge I have with formal verification is that I am yet to see source code that is a perfect implementation of the formal specification.