Summary: In this paper we describe the formal specification and verification of an efficient algorithm based on bitvectors for real-time model checking with the KIV system. We demonstrate that the verification captures the essentials of the C++ algorithm as implemented in the RAVEN model checker. Verification revealed several possibilities to reduce the size of the code and to improve its efficiency.