# K-Michelson: Verifying Michelson in Michelson
**URL:** https://forum.tezosagora.org/t/k-michelson-verifying-michelson-in-michelson/2128
**Category:** Project Updates
**Tags:** michelson
**Created:** [August 21, 2020, 1:22pm UTC](https://forum.tezosagora.org/t/k-michelson-verifying-michelson-in-michelson/2128 "2020-08-21T13:22:18Z")
**Posts on this page:** 2
**Page:** 1
### Author:  [@runtimeverification](https://forum.tezosagora.org/u/runtimeverification)
#### Post date: [August 21, 2020, 1:22pm UTC](https://forum.tezosagora.org/t/k-michelson-verifying-michelson-in-michelson/2128/1 "2020-08-21T13:22:18Z")
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](https://runtimeverification.com/blog/formal-verification-framework-for-michelson/) that you can check for a bit more detail.
Curious readers are also welcome to take a look at our [GitHub repo](https://github.com/runtimeverification/michelson-semantics) to see our current progress.
Thanks for reading!
---
### Author:  [@tezz](https://forum.tezosagora.org/u/tezz)
#### Post date: [August 21, 2020, 2:00pm UTC](https://forum.tezosagora.org/t/k-michelson-verifying-michelson-in-michelson/2128/2 "2020-08-21T14:00:11Z")
Thank you for the update on your work! It’s great to have such a robust and formally verifiable smart contract language.