Kebutuhan Teknologi Computer Aided Verification dalam industri perangkat lunak jelas tidak diragukan lagi. Namun, metode-metode yang terdapat didalamnya masih memiliki banyak keterbatasan sehingga penerapannya secara umum masih belum terwujud. Artikel ini mempresentasikan sebuah metode verifikasi perangkat lunak yang disebut dengan external embedding menggunakan Theorem Prover HOL. External embedding menghindari kompleksitas dari metode deep embedding dan ketidaklengkapan dari metode shallow embedding. Operasi pembuktian bekerja pada representasi abstract syntax tree dari sebuah program dan spesifikasinya. Metode ini telah diterapkan pada alat bantu verifikasi program yang disebut xMech dan juga untuk alat bantu verifikasi aplikasi database yang disebut LinguHOL.