[Genbox]

I've always said that computer science has a PR problem.

Formally verified applications is such a foreign concept to people that when you say "verified correct" they get skeptical and mistrust the whole concept.

Saying something is "secure" when it has been formally verified will be received with a grain of salt, but it is much easier to say than:

"we wrote a detailed specification that define the whole system via algebra, and then we let a theorem prover run all possible permutations of the specification It has now tested a billion edge-cases and we have reached a state where it no longer finds any deviation from the specification."

At least it is provable better than someone saying "it is secure because we think it is".