You radically overestimate the skills of the average programmer.

You are correct when you say that writing verifiable/verified code is a separate skill that not many programmers possess.

But crucially, it's a skills gap -- not an intelligence gap -- that stands in their way. For most properties, writing verified code doesn't require that much more intelligence than writing normal code. Different skills, but in most cases not much more intelligence.

But I don't think a skills gap is the most pressing barrier. There is an intrinsic difference in difficulty between stating conjectures and proving theorems. There's no silver bullet here, including either education or raw intelligence. The latter is, intrinsically, more difficult and more time consuming.

I'm reasonably sure that for all things where a proof would be helpful, that is properties that the programmer has a nontrivial chance of getting the implementation wrong and not catching the mistake with a test, a correctness proof is a lot harder than writing a correct implementation. I've dabbled a bit with Coq and Isabelle and certainly found this to be the case.

Stronger type systems help a lot with common security problems. Memory safety and a system to express taint of inputs eliminate a huge class of potential problems. They are still very, very far from correctness proofs that could catch actual logic bugs.

In Monte, this object is proven by the compiler/interpreter to be transitively immutable:

  object popsicle as DeepFrozen:
    to getFlavor() :Str:
      # Obviously immutable.
      return "lime"

    to getObservedColor(eye):
      # The eye might not be immutable, but that's still okay.
      # All that's required is that this object not secretly stash the eye.
      return eye.observeCMYK(38, 0, 78, 1)

You radically underestimate the intelligence of your fellow humans.

In C++ the same can be achieved by using "const". I don't think that such properties are very useful in preventing security problems.