Penelitian ini bertujuan untuk melakukan verifikasi pada sistem pengendali lalu lintas kereta api dengan menerapkan metode formal, khususnya model checking. Model checker yang digunakan adalah NuSMV. Penelitian dilakukan sesuai dengan tahapan-tahapan pada model checking, yaitu pemodelan rancangan sistem, spesifikasi syarat keamanan sistem dalam bahasa formal logika temporal, serta verifikasi apakah model yang dibuat telah memenuhi spesifikasi. Selain itu, dilakukan pula analisis unjuk kerja sistem berdasarkan alokasi waktu dan space terhadap parameter tertentu. Hasil penelitian menunjukkan bahwa model checking merupakan metode yang cukup mudah diterapkan dalam melakukan verifikasi pada sistem kritikal, namun membutuhkan sumber daya yang relatif besar untuk verifikasi sistem yang kompleks. Kata kunci: metode formal, model checking, NuSMV, kereta api, logika temporal, verifikasi.