spark2014

I don't know details. GNATprove generates verification conditions (conjectures) from SPARK code and assertations. Then it feeds these verification conditions to proof tool (Why3, Alt-Ergo, CVC4 or Z3). https://github.com/AdaCore/spark2014

> It is very easy to complete a proof on the wrong model That doesn't sound right. Automatic proof assistants/verifiers won't approve your proof unless it really is a proof for the model, right? > there are always errors in the model, at least initially Agreed. > There's always an iterative process of refining the model until you are confident in its being good enough. When are you confident it is good enough? It's true that bugs in the model are a possibility. More broadly, it's possible for defects to get through a formal software-development methodology. There was an interesting case study done on this. [0] Vastly fewer than if formal methods are not used, but you're still right that ultimately it's not a completely rock-solid guarantee. (And that's not counting things like bugs in the proof-assistant, or bugs in the non-verified compi

So it has typestates. (I recommend anyone [0] and its HN thread [1] for detail.) I think that's a great language feature for helping to avoid bugs, especially the kind that often happen in C, but I don't imagine it's anywhere close to proving whole-program correctness, is it? For the curious, here's an official example in the SPARK language, that gives a proven-correct sort function. (A complete proof of correct program behaviour, not just absence of undefined behaviour). As you can see, proving correctness is a challenge that permeates every inch of the code. [2][3] Microsoft's Dafny language is similar. [4] [0] https://yoric.github.io/post/rust-typestate/ [1] https://news.ycombinator.com/item?id=21413174 [2] https://github.com/AdaCore/spark2014/blob/76e08d279c/docs/ug... [3] https://github.com/AdaCore/spark2014/blob/76e08d279c/docs/ug..