Formal Methods: Just Good Engineering Practice?

Marc Brooker, an engineer at Amazon Web Services, argues in his TLA+ conference keynote that formal methods are not a costly overhead but a time and money saver for large-scale, distributed systems, or critical low-level systems. By reducing rework and the cost of change, formal design significantly improves software development efficiency. Not all software benefits; agile development is better suited for areas sensitive to changing user requirements, such as UIs or pricing logic. However, for large systems with well-defined requirements, formal methods effectively reduce bug rates and improve performance. Brooker recommends various tools, including specification languages like TLA+, P, and Alloy, model checkers, and verification-aware programming languages. He emphasizes that formal methods not only ensure correctness but also help explore optimization options, avoiding the difficult trade-off between correctness and performance.