Even though Cryptol version 2 is too new to have any questions actually be “frequently asked”, we anticipate the following ones, and will add answers to questions that are actually frequently asked to this list:
How is version 2 different from previous versions of Cryptol? Here is a document that summarizes the changes in the syntax of Cryptol version 2. The other major change is that the more complex verification functions have moved from the Cryptol interpreter to the SAW tools.
How can I be assured this is safe to use? Answering this question was a significant factor in our decision to release the source code to Cryptol. Everything we release in our binary distribution can be built from the source on GitHub.
What else can you do with Cryptol? Cryptol is a powerful tool for
harnessing the power of SMT Solvers like Yices, Z3 and CVC4. The
examples/funstuff folder has solutions to problems like Sudoku encoded
in Cryptol, which then can be solved using the :sat command. In
combination with the SAW tools, Cryptol can
be used to verify that implementations of cryptographic algorithms in
languages like C or Java match their specification. We are continuing to
evolve the capabilities of Cryptol, and those enhancements will be
incorporated to the release on GitHub.