1. 1

This work verifies properties of a pacemaker written in C with that verified against a model written in Promela for SPIN model-checker. The combo of C and SPIN is notable given one is dominant in embedded with the other easy for developers to learn and affordable to use vs most formal methods. SPIN has been finding protocol or time-related errors for over a decade in industry with many use-cases similar to TLA+.