Teknologi verifikasi berbantuan komputer digunakan untuk membantu pembuktian kebenaran perangkat komputer yang dikembangkan dengan menggunakan metode formal. Secara garis besar, terdapat dua macam teknologi penunjang tersebut, yaitu model checking dan interactive theorem proving. Interactive theorem proving menggunakan aksioma dan teori-teori serta aturan inferensi yang sudah terjamin kebenarannya dalam membuktikan suatu teorema. Hal ini mengakibatkan interactive theorem prover lebih dipercaya daripada model checker yang melakukan pembuktian dengan menggunakan algoritme. Tetapi dalam interactive theorem proving, pada dasarnya pengguna harus memikirkan langkah-langkah pembuktiannya. Sedangkan dalam model checking, komputer yang akan secara otomatis menguji apakah sebuah sistem memenuhi spesifikasi tertentu. Penelitian ini bertujuan untuk mengintegrasi teknologi dari model checker dengan interactive theorem prover. Hal tersebut dilakukan dengan memodifikasi kerja model checker agar menghasilak skrip yang dapat digunakan sebagai masukan langkah pembuktian bagi interactive theorem prover, disamping pembuktian untuk model checker itu sendiri. Implementasi dari model checker dilakukan dengan menggunakan Bahasa Pemrograman Fungsional Gofer (Jones, 1991).