[tommd]

Some recent happenings in Cryptol land include:

  * Dylan recently released a literate Cryptol version of the CFRG's ChaCha20/Poly1305 document.  Very cool to see more Cryptol code like this.
  * Merged the fork of SBV with upstream.
  * ABC is now a supported prover.
  * Support for parallel (first to finish) proving using ':set prover=any'.
  * The type checker has been revamped for v2.3, so we should see simpler constraints "soon".

[CHY872]

Parallel proving should be a big bonus. Nipkow found that on the Isabelle test set, using 3 theorem proves in parallel gave as good results in 5 seconds as the best among them gave in 120.