I don't know about DSLabs' model checker but the advantage you get from TLA+ is that it's plain, simple maths. It can be used for specifying systems at many lev

I don't know about DSLabs' model checker but the advantage you get from TLA+ is that it's plain, simple maths. It can be used for specifying systems at many levels of abstraction that a programming language cannot. I'd be curious about how expressive DSLabs' language is, being based on Java -- can it express temporal properties as well as safety properties? As well the TLA+ toolbox has other tools in addition to the model checker: a pretty printer, and a proof system as well.