Hedera Stablecoin - Formal Model

This formal specification of Hedera Stablecoin has been developed by Jan Gorzny, Kacper Bak, Ed Zulkoski, and Don Ho from the Quantstamp Team (https://quantstamp.com/).

Introduction

The K Framework makes it possible to rigorously verify specifications. We make many assumptions like those of the EVM and provide a specification of a stablecoin.

Structure

Specifications are formalized in files ending in -spec.k.

Usage

To run, we recommend the docker version of the K-framework. Then to run the commands in the k framework, you can do the following.

1. Checkout this repo somewhere.
2. Run docker run -it -v /your-path-to-this-repo/hedera-stablecoin:/root/hcs runtimeverificationinc/kframework-k:ubuntu-bionic-bbc70cb
3. cd root/hcs
4. make (to build and prove all the specifications)

Alternatively, you can build the main module: kompile --backend java hcs.k

and prove a single specification: kprove compliant-spec.k (or any other file ending in -spec.k)

Proving a specification should output #True (and maybe some warnings).

Acknowledgments

Based on the ERC-20 Formal Model of Grigore Rosu.