Supporting Correct Intermittent Computing at the Extreme Edge

Batteryless, energy-harvesting devices (EHDs) are a new class of embedded computing platform that are powered solely by energy collected from the environment, without using batteries. These devices enable new applications in domains like disaster monitoring, body implants, or smart city infrastructure. Unfortunately, environmental energy is scarce, so EHDs are powered only intermittently, experiencing frequent failures that make correct programming difficult. The field of intermittent computing seeks to overcome the correctness and programmability challenges introduced by these power failures but has historically relied on ad-hoc correctness reasoning that provides no guarantees, limiting the effectiveness of EHDs as many of the envisioned application domains have high assurance requirements. This talk presents my research in leveraging formal methods and programming language techniques to design systems for EHDs that have provable correctness guarantees. I will cover the basics of intermittent computing; my recent work in designing formally correct intermittent systems for sequential, single-node platforms; and my ongoing work in supporting more complex, concurrent platforms. Throughout, I will highlight the importance of modularity and abstraction in both formalism and system design and how that connects to my end goal of creating full-stack verification pipelines for emerging computing platforms.