Absolutely, none of the current formal methods approach scale to the level of much commercial software. Much of the systems engineering work that we did at Altr

Absolutely, none of the current formal methods approach scale to the level of much commercial software. Much of the systems engineering work that we did at Altran was focused on minimising the extent of the system that would need the higher levels of verification. So flow analysis and absence of runtime error proofs were commonplace, but proof of correctness against the spec was something that was much more focused on specific very high integrity components. I remember thinking that B was a heck of a lot of work for event the smallest projects. I'm kind of surprised that it's still being used.