Vom Nutzer wird relativ viel Eingreifen verlangt, so muss er nicht nur den Zustand angeben, sondern auch noch Klassen von unereichbaren Zuständen definieren. Zu Beginn der Entwicklung musste er dann manuell die Informationen auswerten, später hat der Analyzer dann selber unereichbare Zustände ausgeschlossen, die dennoch zuerst bestimmt werden mussten. Mit Hilfe des automatischen Modus kann man, so man mit Hilfe des State Unifiers und des Language Checkers, eine Menge unereichbarer Zustände definiert hat, bei vielen einfachen Protokollen, Fehler relativ einfach finden. Der Analyzer wird hier aber immer weiter eintwickelt, wie oben erwähnt, kann er mittlerweile automatisch unerreichbare Sprachen finden. In [8] wurde mit Hilfe des Analyzer das Internet Key Exchange Protokoll untersucht (z.B. in Verwendung bei vpn) und der Analyzer erweitert um auch komplexe Protokolle vernünftig untersuchen zu können. Leider findet man über den genauen aktuellen Stand wenig Information.
Der ,,NRL Protocol Analyzer`` ist in Quintus Prolog und SWIProlog impelementiert und wurde verwendet um zahlreiche unbekannte Fehler in Protokollen zu finden, wie z.B. im Simmons Selective Broadcast Protocol und im Burns-Mitchell Resource Sharing Protocol.