Batteryless, energy-harvesting, intermittent computing platforms can be deployed indefinitely in environments that are unsuitable for traditional embedded devices, such as disaster zones, body implants, or even tiny satellites, enabling exciting new applications across bio-medical, disaster monitoring, and defense domains. The major challenge hindering this advancement is that harvested energy is unreliable and causes frequent power failures that introduce new errors and bugs in software running on the platform. Such errors make these platforms unsafe for applications, e.g., in health and defense spaces, where bugs could cause significant harm, either by accident or by a malicious party exploiting the bug. The goal of this project is to build up both theory and practical tools to create an embedded operating system (OS) that is verified (i.e., proven by machine) to execute applications correctly and securely through power failures. The project's novelties are that it defines the first formal model of an intermittence-safe OS and develops new programming languages and verification frameworks for proving that intermittent system implementations satisfy their correctness and security requirements. Such verification tools integrate into AI-based code generation workflows and make writing correct software much easier, as coding agents can write proofs and developers can check that AI-generated code meets requirements. The project's impacts are that it makes intermittent computing platforms trustworthy to run sophisticated safety-critical applications in previously inaccessible deployment environments; that it gives developers tools to write verified intermittent system software, either directly or through AI workflows; and that it supports the education of a future workforce who can create provably well-behaved system software, reducing costly bugs and cyber-attack vectors. To accomplish its objectives, the project pursues four major thrusts. The first thrust devel