Perhaps because their concerns are different? Similar reasoning: "why invest in dependently typed languages over SMT solvers? SMT solvers are automatic, and it is way easier to add annotations to my programs"

The answer is that these technologies are not universal in trade off space.

Of course, if you can have an LLM prove something by dispatch to an SMT solver ... you want to do that (and, indeed, LLMs do sometimes do this even when working on Lean proofs)

But the space of statements that you can prove using verification with SMT is smaller than dependently typed systems.

Also, Ada/SPARK are very good and robust -- they've been around for ~50 years ... but there's been a significant amount of work in formal verification since then, right? I would be more clear that Ada/SPARK are state-of-the-art for "mission critical software" (and have been for many years), but there's been a lot of research work in formal verification of low level programming since then (Low*, for instance)