Re: Announcing Sbuilder - a tool to generate TLA+ model for business IT systems

I have released a tool, sbuilder-ethereum, which translates Ethereum
Solidiy language implementations to TLA+.

The idea of the tool is to translate (subset of) a simple language,
such as Solidiy, into formal model, allow users to define correctness
criteria (currently in TLA+ language), allow users to define
environment model aka 'setups' (~tester on steroids acting on the
formal model - and limiting state space explosion). Benefits: increase
confidence to application correctness, and make QA more efficient with
faster feed back.

Current status 'pre-alpha'

Some links:
* sbuilder-ethereum tool MIT license https://github.com/jarjuk/sbuilder-ethereum
* on-line documentation (translation reference & cucumber tests): http://jarjuk.github.io/sbuilder-ethereum/0.0.6/FEATURES.html
* an overview of the tool in blog post https://jarjuk.wordpress.com/2016/12/08/sbuilder-ethereum-announce
* an example of using the tool https://jarjuk.wordpress.com/2016/12/09/sbuilder-ethereum-example
* for more background information https://jarjuk.wordpress.com/sbuilder/

A gist with a solidity contract and translated TLA result
for one setup. Some benchmark results (using Intel(R) Core(TM) i7-4702MQ CPU @
2.20GHz)

* generated TLA+ model.tla file 13415 lines long
* 619 states generated, 585 distinct states found, 0 states left on queue.
* timing
** generate: real 0m7.757s, user 0m7.600s, sys 0m0.160s
** model checking: real 0m3.863s, user 0m14.722s, sys 0m0.458s

All pointers to similar tools most welcome. Especially would like to see an example, how to document translation semantics.

Next: update road map