That’s interesting you say that. I’ve known two engineers who worked at JPL and they said that no teams did anything close to formal verification. It’s an incredibly difficult bar to meet
She/He is right and I was a bit cynical in my answer. There are some real industrial projects that used formal methods. I have in mind Airbus with ASTREEE, the Meteor subway system (Paris' subway line 14), Windows' drivers with the SLAM analyzer...
Also, JPL released its model-checker Java PathFinder and hosts every year the Nasa Formal Method conference so I'm pretty confident that at least someone at NASA is interested in formal methods =)
Also, JPL released its model-checker Java PathFinder and hosts every year the Nasa Formal Method conference so I'm pretty confident that at least someone at NASA is interested in formal methods =)