形式化方法只能解决一半问题：分布式系统设计的局限

形式化方法如TLA+和P在验证系统安全性和活跃性方面非常有效，但只能解决分布式系统设计中的部分问题。作者提出，延迟、成本、硬件需求等关键问题需要通过原型设计、建模和模拟来解决。他呼吁开发新工具，结合形式化模型和性能分析，以提供更精确的定量设计洞察，帮助行业实现更高效的系统优化。