I don’t know anything about SPARK or FramaC, but TLA+ isn’t a programming language, and you can use it to model distributed functional apps just fine (I still do).
Even if the Erlang/Ericsson stuff is the “only case” (It’s not) I do not see how that makes my point less valid; Erlang was specifically design for systems that cannot fail. Telephones are just a good example of that.
And doesn't your TLA+ model make your functional code significantly more reliable? Guess what, it does the same thing for OO languages => no need to use FP to increase reliability.
Same goes for the other tools or languages I mentioned.
Even if the Erlang/Ericsson stuff is the “only case” (It’s not) I do not see how that makes my point less valid; Erlang was specifically design for systems that cannot fail. Telephones are just a good example of that.