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.

  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)