search

runtimeverification / michelson-semantics

A K semantics of Tezos' Michelson language.
Other
17 stars 8 forks source link

Migrate from `kprove` to `kprovex` #353

Open Baltoli opened 2 years ago

Baltoli commented 2 years ago

The specs used in this project rely on [token] definitions for syntactic convenience. These should be kompiled into a separate module so that kprovex can be used.

For context, we are deprecating kprove: https://github.com/runtimeverification/k/issues/2490