Teknologi perangkat lunak berbasis komponen adalah sebuah trend yang menjanjikan dalam pengembangan perangkat lunak. Hal ini disebabkan oleh sifat reusability dari sebuah komponen, dimana komponen dapat digunakan kembali dan dikomposisikan menjadi aplikasi yang diinginkan. Konsep perangkat lunak berbasis komponen ini didasari oleh komponen dalam bidang elektronika, dimana pihak yang ingin mengembangkan suatu alat elektronika tidak perlu mulai dari awal untuk tiap alat baru. Untuk merealisasikan hal tersebut untuk perangkat lunak, ada banyak tantangan yang harus dihadapi. Salah satu tantangan tersebut adalah masalah sertifikasi. Penelitian ini mempelajari tentang sertifikasi perangkat lunak berbasis komponen, dengan studi kasus aplikasi E-Voting. Dalam penelitian ini, penulis mencoba menerapkan logika UNITY dalam mempelajari studi kasus aplikasi EVoting tersebut. Selain itu, penulis juga menggunakan HOL theorem prover sebagai alat bantu dalam pembuktian.