Yes, I think that is one of the big weaknesses of it. You can write specs that make no sense and it will just let you. So far there is also no way to automatic

Yes, I think that is one of the big weaknesses of it. You can write specs that make no sense and it will just let you. So far there is also no way to automatically check whether you are strengthening a guarantee or weaken your assumptions relative to a previous spec. In a perfect world we would have this in my opinion.