Blog
News, notes and technical reports from the CryptWalker project.
-
CryptWalker has a website
CryptWalker now has a home on the web. Besides this blog, the site hosts the API reference, generated by doc-gen4 straight from the Lean sources for every module, definition and lemma in the library.
Future posts will cover how individual primitives are specified and proved, and how we check them against reference implementations.
Read more