How to do safety check in TmJests algorithm?

I am doing reachability analysis of my system. I have seen in example using assert to do checks on the system. But 
I want to know is there any way by which specification can be put into the problems itself to make a safety check automatically. 

Thanks in advance