Layanan web muncul sebagai tren baru dalam pemenuhan kebutuhan berkomputasi. Banyak sistem baru muncul dan memanfaatkan komunikasi antar layanan web. Sistem baru tersebut dapat dipandang sebagai komposisi antar perangkat lunak. Penelitian ini mengangkat studi kasus SIBAYAR, sistem keuangan perguruan tinggi dan berasal dari layanan-layanan web yang independen. Formalisasi perangkat lunak dimaksudkan untuk memverifikasi kemampuan dan tingkat kepercayaan suatu perangkat lunak dalam menjalankan fitur-fiturnya. HOL theorem prover hadir sebagai salah satu alat formalisasi perangkat lunak berbasis pembuktian, semi otomatis, dan didasari oleh logika orde tinggi dengan aturan-aturan penalaran yang sound. SIBAYAR diformalisasi dengan HOL theorem prover dalam kerangka berpikir bahwa SIBAYAR adalah komposisi perangkat-perangkat lunak independen. Formalisasi SIBAYAR dilakukan di atas kerangka kerja UNITY, salah satu kerangka kerja penulisan program dan formalisasi konkuren. Sebelum formalisasi dilakukan, eksplorasi meliputi pembuktian Hukum de Morgan dan verifikasi rancangan digital dilakukan untuk memberikan pengalaman bekerja di dalam lingkungan HOL theorem prover.