In diesem Beispiel wird beispielhaft eine Eigenschaft eines Modulo 3 Zählers überprüft. Zunächst muss dazu die Gatterschaltung in das Zustandsübergangsdiagramm umgewandelt werden. Dies geschieht im realen, OBDD-basierten Modelchecker jedoch nur implizit durch Aufstellen der OBDDs. Der Check-Prozess ist hier animiert dargestellt und liefert ein positives Ergebnis für die spezifizierte Eigenschaft, d.h. der Zustand [0,0] wird tatsächlich immer (d.h. von jedem anderen Zustand) erreicht.