Yup - if you have control over your code base and can keep it totally consistent you have a fighting chance, but as I say - some shifty person introduces a problem and all goes very very wrong. The big demonstration is that it's really rarely used in industry. Which is a big shame as if we could sort out the programming in the large then I believe big value is on the table. The new generation of reasoners are a good start!