"MALPAS was certainly not used by IPSN as extensively as by NE on Sizewell B PPS. There may be several practical reasons for this, one of them being the considerable investment of effort which large-scale use entails." UK nuclear power stations run C code, not properly formally verified. MALPAS is a static analyser for C.