Terjadinya kematian akibat transfusi darah di Indonesia pada tahun 2015 mengakibatkan keamanan alur penyediaan darah dipertanyakan. Pada tugas akhir ini penulis melakukan verifikasi rantai pasokan darah di Indonesia menggunakan pendekatan metode formal, yaitu Logika Temporal Linier (LTL). Alur pasok darah didapatkan dari PMI (Palang Merah Indonesia). Alur pasok darah dimodelkan dalam diagram aktivitas. Kemudian diagram aktivitas diverifikasi terhadap persyaratan yang diatur oleh kementerian kesehatan. Persyaratan yang didapatkan ditranslasikan ke LTL dan diagram diubah ke dalam model NuSMV. Dari hasil verifikasi menggunakan model-checker NuSMV, dapat disimpulkan bahwa rantai pasok darah di Indonesia terbukti aman secara formal terhadap persyaratan dari peraturan kementerian kesehatan.