Kertas ini membincangkan tentang penspesifikasian dan pengesahsahihan formal ke atas protokol CSMA/CD. Penspesifikasian dilakukan ke atas nod dalam rangkaian dan situasi dalam implementasi bas bagi protokol CSMA/CD. Satu jenis asas, empat jenis bebas, satu pemboleh ubah sejagat, dua skema keadaan dan sembilan skema operasi yang mewakili protokol CSMA/CD telah berjaya dibangunkan menggunakan bahasa formal Z. Kemudian, pengesahsahihan dilakukan ke atas spesifikasi tersebut dengan menggunakan teknik pembuktian teorem yang disokong oleh alatan pembukti Z/EVES. Sembilan teorem telah dibangunkan berdasarkan kepada sembilan operasi yang telah dispesifikasikan. Dari kajian didapati bahasa Z berupaya untuk menspesifikasikan protokol komunikasi. Selain itu, penggunaan alatan sokongan dalam proses pembuktian dapat menjimatkan masa dan tenaga, dan kecenderungan ralat berlaku adalah kecil.