The FARMHANDS project has been a very fruitful experience on using different formal tools as part of the development process, from theorem provers (PVS, Coq) and model checkers (McErlang) to more specific tools, such as tools for the automatic generation of test cases from property definitions (QuickCheck). Tools for performance evaluation of functional applications (tsung) or refactoring tools for distributed functional programs (Wrangler) have been used, too. In some cases (QuickCheck, McErlang), there has even been collaboration for the improvement of these tools, or some ad-hoc tools have been created (VoDKAV took, JWMTool)

Even though the (semi)automatic translation from a program specification to a working implementation is not realistic from an industrial point of view yet, the pragmatic aproximation of test cases automatic generation from system properties definition using a formal language seems excitingly promising and is a huge step forward in the common adoption of formal methods as part of the software development process.