The Power of Reachability Logic
In a previous blog post, we introduced the K-Michelson project, a project developed by Runtime Verification and funded by a generous grant from the Tezos Foundation. So what is K-Michelson? Simply put, it is a formal verification framework for Michelson smart contracts; see our previous post for details. In this two-part series, we will investigate:
- What an ideal programming language specification looks like.
- How this ideal framework powers nextgen program testing.