Tugas akhir ini merupakan penelitian awal dalam usaha membuat formalisasi TLA+ dalam theorem prover HOL. Metode formalisasi yang digunakan adalah Shallow Embedding. Sebelum melakukan formalisasi, dilakukan studi literatur mengenai TLA+, dan studi kasus mengenai spesifikasi buffer komunikasi menggunakan FIFO. Penelitian ini merupakan penelitian eksperimental. Hasil dari tugas akhir ini adalah formalisasi sebagian teori TLA+ dalam HOL. Hasil penelitian ini menyarankan beberapa penelitian lanjutan yang mungkin dapat dilaksanakan, yaitu formalisasi teori TLA+ secara lengkap dalam HOL, dan studi kasus untuk melakukan verifikasi spesifikasi TLA+ dengan theorem prover HOL.