"Transiently powered devices have given rise to a new
model of computation called intermittent computation.
Intermittent programs keep checkpointing the program
state to a persistent memory, and on power failures, the
programs resume from the last executed checkpoint. Intermittent programs are usually automatically generated by instrumenting a given continuous program. The behaviour of the continuous program should be equivalent
to that of the intermittent program under all possible
power failures.

We presents a technique to formally verify
the correctness of an intermittent program with respect
to its continuous counterpart. We present a model of
intermittence to capture all possible scenarios of power
failure, and an algorithm to find a proof of equivalence
of the two programs."