It looks like the docs just talk about the C and Python APIs, and don't talk about the command line tools.

Tut is a documentation tool that lets you write documentation/examples that are automatically typechecked and run. Maybe we can use it for the user manual? Just an idea.

It may be nice to have series of short videos on how to install and/or how to use with a few small examples. One can create these videos using screen recording utilities (such as recordmydesktop for Ubuntu).

This is purely for enhancement of the documentation and user education and is in no way critical for the functionality.

The runtime option for logging (-v) should allow for a reasonable amount of introspection of the checker's behavior. At least we should output the status of each lemma (skipped/RUP/RAT/...). Printing the trail is probably too much though.