Salah satu alat bantu untuk melakukan verifikasi program dengan komputer adalah HOL theorem prover. HOL cukup populer namun memiliki keterbatasan dalam merepresentasikan program. Penggunaan HOL juga cukup sulit dan membutuhkan pengalaman yang tidak sedikit. Untuk mengatasi keterbatasan HOL terutama dalam merepresentasikan program dikembangkanlah xMECH. XMECH adalah pengembangan dari HOL yang memperkaya kemampuan dan interaksi HOL dalam melakukan verifikasi program, sehingga dapat memberikan kemudahan dalam proses verifikasi 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 sehingga belum memiliki antarmuka yang layak. Antarmuka xMECH masih sederhana sehingga pengguna memerlukan usaha yang tidak kecil agar bisa mengerti bagaimana cara menggunakannya. Untuk itu dalam proyek mahasiswa ini akan dikembangkan antarmuka xMECH yang berbasis grafis (Graphical User Interface). Antarmuka ini diharapkan akan membantu pengguna dengan mengotomasi beberapa langkah-langkah pembuktian di xMECH dan memvisualisasikan bagian-bagian yang dapat membantu dalam melakukan pembuktian program. Dengan demikian, pengguna xMECH bisa lebih berkonsentras