هزینه زیاد و تبعات منفی اجرای طرحهای ناقص و آسیب پذیر، باعث شده است که قبل از اجرای هر سیستم حساس و مهمی، همچون سیستمهای رای گیری الکترونیکی، درستی یابی عملکرد آن به امری ضروری و پیش نیاز تبدیل شود. اثبات های شهودی، از درجه دقت و اطمینان بالای مورد نیاز برخوردار نیستند، بنابراین همواره استفاده از روش های صوری برای این گونه اثبات ها پیشنهاد می شود. در این مقاله، با استفاده از حساب پی کاربردی، که یک زبان صوری مبتنی بر جبر پردازهای بوده و توسعهای بر حساب پی می باشد، یک مدل صوری برای پروتکل رای گیری الکترونیکی لین و همکارانش ارایه شده است. همچنین برقراری ویژگی امنیتی صحت، که شامل خصوصیات غیر قابل تغییر بودن، عدم استفاده مجدد و مجاز بودن می باشد، در این پروتکل با استفاده از برهان های مطابقت و به کمک ابزار پرووریف، وارسی و اثبات شده است.