Aren formal methods useless?
No. First of all, they’re already being used for small-scale and narrowly-defined problems. More broadly, current formal methods approaches have trouble scaling up to large systems, and also tend to have trouble adapting to requirements changes. But there’s no fundamental reason this must be so. To be practical, FM must be automated by tools that can handle larger scales and can handle changes more gracefully. What we hope to do is share OSS FM tools that are available, encourage development of implementations and proofs that use those tools, and through this mature both the tools and our understanding of how to best use them. By starting small, we can identify some of the key tool challenges, and feed those back to toolmakers so that they can improve. As those improvements are placed in tools, they can be used to handle larger and larger problems. In addition, larger proved systems can be built by starting with smaller proved systems and components. This will be a long-term process, b
