The SyVOLT Contract Prover
SyVOLT is a contract prover for DSLTrans model transformations. It will guarantee that all inputs including the contract's pre-condition will produce outputs including the contract's post-condition.
Download SyVOLT here.
Here is a video describing SyVOLT.