How does this compare with other formal methods like Z? Has anyone here used them successfully in the field?