Cred ca introducerea mea lasa de dorit mai mult decat subiectul este in sine greu

Dar ceea ce spui tu e adevarat din doua puncte de vedere:
1. problemele de verificare sunt greu de modelat matematic (si deseori greu de rezolvat

)
2. problemele de verificare sunt foarte grele dpdv computational: multe sunt nedecidabile (nu exista algoritmi care sa le rezolve -- caz in care cautam subclase decidabile), altele sunt EXPTIME, NP-complete etc. De exemplu, un adevarat succes in verificarea protocoalelor a fost reprezentat de un rezultat de NP-completitudine pentru verificarea confidentialitatii in cazul unui numar marginit de sesiuni.
Desi problemele de rezolvat sunt demonstrabil "grele" (nedecidabile, NP-complete), multe tool-uri implementeaza algoritmi/semialgoritmi care se dovedesc folositori in practica. Un exemplu de succes este reprezentat de verificarea (partiala) a protocoalelor WS-* de catre Microsoft (
http://research.microsoft.com/projects/samoa/)