Jukka_JJukka_J Posts: 6Member

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 tool, latest 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!



Sign In or Register to comment.