Salah satu alat bantu untuk melakukan verifikasi program dengan komputer adalah HOL theorem prover. HOL cukup populer, namun memiliki keterbatasan dalam mempresentasikan program. Penggunaan HOL juga cukup sulit dan membutuhkan pengalaman yang ditak sedikit. Untuk mengatasi keterbatasan HOL terutama dalam mempresentasikan program dikembangkan xMECH. xMECH adalah pengembangan dari HOL yang memperkaya kemampuan dan interaksi HOL dalam melakukan verfikasi program. xMECH dikembangkan oleh Ade Azurat dan I.S.W.B. Prasetya sejak 2001 di Institute of Technology and Computing Science, Universitas Utrecht. Saat ini, xMECH masih dalam tahap prototipe dan belum memiliki antarmuka yang layak. Antarmuka xMECH masih sederhana sehingga pengguna memerlukan usaha yang tidak kecil agar bisa mengerti cara menggunakannya. Untuk itu dalam proyek mahasiswa ini telah dikembangkan antarmuka xMECH yang berbasis grafis (Graphical User Interface). Antarmuka ini membantu pengguna mengotomasi beberapa langkah-langkah pembuktian di xMECH dan memvisualisasi bagian-bagian yang dapat membantu dalam membuktikan program. Pada xMECH sekarang, pengguna masih harus berhubungan langsung ke HOL. Dalam antarmuka ini ouput dan ri HOL ditampilkan secara visual dengan proses parsing. Parsing yagn ada saat ini, masih sederhana dan belum memiliki spesifikasi grammar yang lengkap, tetapi hanya berupa lexical analyzer.