# K-Michelson: a Case Study on Formal, Executable Language Specification **URL:** https://forum.tezosagora.org/t/k-michelson-a-case-study-on-formal-executable-language-specification/2384 **Category:** Project Updates **Tags:** michelson **Created:** [November 6, 2020, 5:03pm UTC](https://forum.tezosagora.org/t/k-michelson-a-case-study-on-formal-executable-language-specification/2384 "2020-11-06T17:03:26Z") **Posts on this page:** 1 **Page:** 1
### Author: ![runtimeverification](https://forum.tezosagora.org/letter_avatar_proxy/v4/letter/r/45deac/32.png) [@runtimeverification](https://forum.tezosagora.org/u/runtimeverification) #### Post date: [November 6, 2020, 5:03pm UTC](https://forum.tezosagora.org/t/k-michelson-a-case-study-on-formal-executable-language-specification/2384/1 "2020-11-06T17:03:26Z")
Hello again! This is Stephen Skeirik from Runtime Verification. Some time ago, we introduced K-Michelson: a formal verification framework for Michelson [in this post](https://forum.tezosagora.org/t/k-michelson-verifying-michelson-in-michelson/2128). Today, I’d like to give some brief updates on progress we have made: 1. We added native support for most Michelson macros, even the old ones. This means tests like the following will run: 2. We added support for reasoning about more symbolic data structures including symbolic `map` and `lambda`. This lets us check that symbolic map updates work as expected. A small example: 3. We have removed lots of legacy code and updated our documentation. This makes it easier to get started and to contribute. We have more updates planned in the near future—continued improvements to our documentation, making our syntax more consistent with upstream, and further refinements to our tooling to increase the range of programs that we can reason about. I recently wrote a [small blog post](https://runtimeverification.com/blog/k-michelson-a-case-study-on-formal-executable-language-specification-part-1/) about our overall vision at Runtime Verification and how that applies to K-Michelson. Feel free to check it out! Finally, if this kind of thing interests you, our [GitHub repo](https://github.com/runtimeverification/michelson-semantics) is always a click away.