- The tutorials for proof annotations and the Proof Checker
- The VC_View and PCHIF** tools
- The high integrity data structure examples.
** The version of the Proof Checker in the GPL 2010 release has an
(apparently unintended) change in the way that it handles I/O -
consequently is will not work with PCHIF. (The Proof Checker in the
previous release - 8.1.1 - works correctly with PCHIF.)