This is the SparkSure homepageSparkSure is an independent consultancy offering services in the production of high-integrity Ada.
Contact details are here.
There are two tutorials for using the proof features of SPARK:
one for the optional proof annotations (for proof of absence of run-time error)
and one for the SPADE Proof Checker.
Details of these are on the SPARK Proof Tutorials page.
We also have a number of tools that help with using the proof features of the SPARK Toolset.
Details of these are on the SPARK Proof Tools page.
High Integrity Data Structures
SPARK has the potential for creating high integrity data structures and the current information on what we have developed is on the Data Structures page.
This now includes the initial release of the red-black tree code, along with the key rules for proving correctness of the code that modifies the tree structure.
The Tokeneer code is an excellent example of SPARK, but the work was completed several years ago and prior to major improvements being made to the proof capabilities of the SPARK Toolset.
I have updated the proofs to make them a better example of how to use user rules and other proof features of the SPARK toolset.
The updated files for the Tokeener reproof including a note describing the changes made and a readme for the updated files are on the Download page.