Many important theoretical and practical advances have taken place in the areaof Formal Methods (FMs), and impressive applications have been developed.Furthermore, FMs and their associated tools are now routinely used in manyindustries. However, their full potential remains partly unexploited. In pg. 57 ofa recent FMs survey [47], I gave my own view about their future in a positionstatement where, among other things, I said (emphasis added):Rather than focusing mostly on [code] verification, [formal methods]should support system design, validation, evolution and maintenancefrom theearliest stages. For this, use ofexecutable formal specificationsfor fast system modeling and analysisbefore implementationis crucial.The problem at present is that many complex systems are still designed in aninformalmanner. This happens not just for the proprietary designs of manycompanies, but even when international bodies responsible for agreeing on andcarefully documenting the standards of a widely used system —e.g., a new com-munication protocol, or a programming language— capture its design mostlyinformally. Let me give three examples that I know well. he second point is illustrated by the systems (1)–(3) described above, which allhad heavily tested, mature implementations.1But the first point is much moreimportant than the second, for the simple reason thatdesign errors are typicallyseveral orders of magnitude more expensive than coding errors.Let me further comment on these two points: formal executable specificationscan be used in two different ways: (i) in apost factoanalysis of an alreadyimplemented system, or (ii) one can use formal executable specificationsaborigine, that is, from the earliest stages of a system’sdesign. As the aboveexamples (1)–(3) illustrate, formal executable specifications can be extremelyvaluable in apost factospecification and analysis of a system. However, postfacto specification and analysis is neither the most cost effective nor the mostfruitful application of FMs for three reasons.