Howdy All! This is Stephen Skeirik from Runtime Verification.
Today, I’d like to introduce you all to K-Michelson—a project we have been working on as part of the Tezos Ecosystem Grants program. K-Michelson is a framework for writing symbolic tests over Michelson code using Michelson as our assertion language. By symbolic, I mean that, for example, instead of checking that:
PUSH int 17 ; PUSH int 0 ; MUL ; PUSH int 0 ; COMPARE ; EQ
we can check that:
PUSH int $x ; PUSH int 0 ; MUL ; PUSH int 0 ; COMPARE ; EQ
which proves that Michelson arithmetic satisfies the basic property x * 0 = 0 for all integers x. By assertion language, I mean that the we write assertions about Michelson program states using Michelson code, like the expression above. This means we don’t have to learn some new language like first-order logic (e.g. ∀x∈ℤ.x * 0 = 0). Of course, the program/assertion above is intentionally simple for illustrative purposes. In practice, we will want to assert richer properties about complex programs. During this grant, we have been steadily increasing the number of Michelson features that we support and programs that we can verify. At this point, the tool still has many sharp edges—once the core features are in place, we plan to spend time to improve the UX.
I recently wrote a blog post that you can check for a bit more detail.
Curious readers are also welcome to take a look at our GitHub repo to see our current progress.
Thanks for reading!
