Designing Formally Correct Intermittent Systems

This lecture by the instructor focuses on designing formally correct intermittent systems, exploring the challenges and solutions in ensuring correctness, reliability, and security in extreme edge computing platforms. The lecture covers topics such as defining correctness conditions, enforcing memory consistency, handling timing constraints, and using type systems for safe intermittent execution. Various tools and formal models are discussed, including Curricle for type-based reasoning and Ocelot for enforcing fresh and consistent inputs. The lecture emphasizes the importance of HW/SW co-design, language abstractions, and security considerations in building robust intermittent systems.