[Raphael_Amiard]

> For verification in general, is the expense of verification in this case because of the model needed to verify Ada? For instance, perhaps a language that makes different choices might have a model checker that could scale better.

I don't think so. The SPARK subset has been chosen to aid verification. The problem of proof is inherently computationally hard, and the most gains you can expect will come from advances in solver technology, both algorithmic and in terms of scaling to multiple cores or GPU eventually.

Just my opinion :) But I work at AdaCore (not on SPARK) so have some familiarity with the subject.