by
David Hauzar
![](https://blog.adacore.com/uploads/_300x300_crop_center-center_none/01_saturate.png)
SPARK 16: Generating Counterexamples for Failed Proofs
While the analysis of failed proofs is one of the most challenging aspects of formal verification, it would be much easier if a tool would automatically find values of variables showing why a proof fails. SPARK Pro 16, to be released in 2016, is going to introduce such a feature. If a proof fails, it attempts to generate a counterexample exhibiting the problem. This post introduces this new feature, developed in the scope of the ProofInUse laboratory.