[yannickmoy]

Here, we are targeting full functional specification, which is hard. So there is a lot of ghost code to support the proof (the loop invariants, assertions and ghost entities). That's what's driving the verification time up. I don't find this enormous at all, given the guarantees provided.

Most code in SPARK is proved to a much more modest level, where the proof is much easier, and that's where you get scaling.

And yes, we're using the best available provers for the task under the hood (currently Alt-Ergo, CVC4, Z3 and COLIBRI), and on some of the checks in that proof of the light runtime, a call to a single prover on a single check may take minutes.