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
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 =)