I have been implementing a tool called 'Sbuilder-ethreum', which creates formal model in TLA+ language
for solidity contracts using AST from solc compiler. An overview.jpg
Currently, I have focused on implementing execution framework (See flow diagram
, and most of the Solidity language implementation is missing. Cucumber tests
constitute the most "authorative" statement of implementation status.Reference document
documents TLA translation and contains also a (partial) TODO list. In short, I am planning to "teach" sbuilder-ethreum to deal with common patterns
starting with withdrawals
Some background information: 'sbuilder-ethereum' is Ruby GEM, which adds ethereum support to sbuilder
. I have written some blog entries on sbuilder
of which explains, how I got started with sbuilder-ethereum.
I am planning to publish the tool under MIT licence, at some point, when the tool does something useful (more than just "Hello World"
. In the mean time, I will update the documents linked here, and add a notice to this post.
Any comments are most welcome!