Summary
Woodcock et al. surveyed 62 industrial projects that used formal methods, spanning aviation, rail, semiconductor, and financial systems. The findings challenge the common perception that formal methods are impractical: most projects reported reduced defect rates and overall cost savings, particularly when specification was applied early. The paper catalogs which notations were used (Z, B, VDM, Alloy), at what development stages, and what barriers teams encountered.
What it means for our work
This paper is the empirical backbone for our thesis that rigor pays for itself. The survey’s key finding — that specification catches defects earlier and cheaper — is exactly the economics we believe AI changes further. If formal methods already showed positive ROI with manual specification effort, the equation becomes even more favorable when AI handles the notation. The 62 projects also validate that Z and B (both supported by Z Spec) have real industrial track records, not just academic ones.