Sbuilder Ethereum Example

Introduction

This post presents an example using Ethereum Solidity language withdrawal pattern to demonstrate, how tla-sbuilder with sbuilder-ethererum plugin can be used to check for implementation correctness.

For an overview of sbuilder-ethereum refer to Sbuilder Ethereum Announcement blog entry.

:More:

Advertisements

Announcing Sbuilder Ethereum

Introduction

This post announces sbuilder-ethereum, a tla-sbuilder plugin, to translate Ethereum implementations in Solidity language into in TLA+ language formal models to be model checked using TLA+ Tools.

:More: