K-Michelson: a Case Study on Formal, Executable Language Specification Part II

Project Updates
1

Hello all! This is Stephen Skeirik from Runtime Verification.

This update is a continuation from last time. For this update, we have been focusing on tidying up our repository and general maintenance. Some highlights:

  1. Updating our user documentation to better explain how to use the K-Michelson tools. We now have a complete walkthrough available in our user guide.

  2. Cleaning our Michelson grammar to better match the syntax of the upstream Tezos client reference implementation. For developers, this means that tests can more easily be ported between the two implementations.

  3. We also have one exciting in-progress item: updating our GitHub pages documentation website theme to be more clean, modern, and usable. This should land in the next couple of days and will be available here: https://runtimeverification.github.io/michelson-semantics/.

We have an accompanying blog post which continues the discussion started in our previous blog post about how we can use K-Michelson to do formal verification.

3 Likes