This small example shows the implementation and proof of the so-called Fulcrum in SPARK, to answer the third problem of this challenge.
This code is referenced in an AdaCore blog post. However, the repository has changed since the appearance of the article. Please use the article tag to see the code that corresponds to the article.
You can verify the proof using SPARK as follows:
$ gnatprove -P fulcrum --report=all --level=2
and compile and run the simple test case as follows using GNAT Pro:
$ gprbuild -p -P fulcrum
$ ./obj/test_fulcrum