This paper presents a method for runtime verification of microcontroller binary code based on past time linear temporal logic ( ptLTL ). We show how to implement a framework that, owing to a dedicated hardware unit, does not require code instrumentation, thus, allowing the program under scrutiny to remain unchanged. Furthermore, we demonstrate techniques for synthesizing the hardware and software units required to monitor the validity ofptLTLspecifications.