Metode formal merupakan metode untuk mendeskripsikan sebuah sistem secara akurat dan tidak ambigu, dan didasarkan pada matematika. Dalam pemrograman, metode formal dimanfaatkan untuk mempresentasikan spesifikasi dari sebuah program secara akurat. Metode formal dalam pemrograman didasari oleh teori yang disebut programming logic yang memungkinkan pengembangan program dari spesifikasinya secara bertahap mendekati bentuk implementasi, dan juga verifikasi atau pemeriksaan kebenaran program. Programming logic digunakan untuk mendekomposisikan program menjadi bagian-bagian kecil yang dapat dibuktikan secara trivial. Interactive theorem prover (ITP) merupakan teknologi yang menunjang penggunaan metode formal. Dalam ITP, komputer digunakan untuk melakukan pembuktian secara interaktif. Salah satu contoh ITP mutakhir adalah Higher Order Logic (HOL). Banyak kelas sistem atauu spesifikasi yang terepresentasikan dengan kalkulus predikat, dapat direpresentasikan dan diverifikasi dalam HOL. HOL mendukung forward dan backward proving. Dasar logika dari HOL dapat diperluas dengan berbagai teori. Dalam tugas akhir ini dikembangkan lingkungan untuk berekperimen dengan programming logic dalam HOL. Programming logic yang mendiskripsikan suatu bahasa sekuensial diimplementasikan fungsi-fungsi untuk medekomposisikan program. sehingga pengguna dapat memanfaatkan fasilitas backward proving HOL untuk melakukan proses verifikasi program secara interaktif.