K-Michelson is:
a formal, executable, and human-readable semantics of the Michelson blockchain programming language using the K framework;
a unit test framework for Michelson programs that allows testing program behavior at a finer granularity than contract invocation;
a formal verification framework for Michelson programs using a slight extension of Michelson as an assertion language.
Serve as a human-readable and executable reference document specifying how Michelson programs should operate.
Provide tools for testing and verifying Michelson programs operate as designed.
Provide a complete formal model of the Tezos blockchain. In particular, we do not model things like: networking and peer-to-peer communication, block baking or validation, transaction pools, protocol amendment, etc.
Replace existing Tezos CLI tools. Developers should still use
tezos-client
for interfacing with Tezos nodes, tezos-node
for running
your own nodes, etc.
See INSTALL.md for installation instructions.
See USER_GUIDE.md for usage instructions.
The project has a very simple layout. Source files live at the project root.
syntax.md specifies the syntax of Michelson and other input data
common.md specifies common infrastructure used in the type checker and the core semantics
types.md contains a rudimentary type-checker for Michelson
michelson.md specifies:
MICHELSON-CONFIG
)MICHELSON
)compat.md is a compatability layer between K-Michelson and the Tezos Reference client used for cross-validation testing
Other directories include:
/ext
- Git submodules for our direct dependencies/hooks
- C++ definitions which implement some low-level operations/lib
- scripts used by the test harness/media
- source code for presentations about K-Michelson/tests
- source code for all testsSee the tests README for more information on test formats and organization.