Version 1.0 of SPARKRules is available from:
The download includes documentation for the tool, a Windows
executable, all the source code (which has also compiled and run on
openSUSE) and, as an example of its use, reworkings of the proof rules
in Tokeneer Version 2.
SPARKRules separates the storage of user rules from the context in
which they are applied, so the documentation includes a discussion of
the potential for unsound proofs to result from this and suggests an
approach to avoid this problem.