FMitF: Track III: Introducing Verification Through Creative Embedded Systems

The project integrates formal verification techniques into creative technology education. It targets students working with microcontroller-based embedded systems and interactive media, including sound synthesis and art installations. As programmers in general, and especially creative technologists, increasingly use Artificial Intelligence (AI)-assisted tools to write code, they face growing challenges in managing and verifying the correctness of their systems. The project’s novelties are its integration of runtime verification, model checking, and reactive synthesis into creative embedded systems curricula, and its adaptation of these tools for use by non-verification students. The vision is that program verification is deeply integrated into every student’s experience, even if they are not explicitly studying verification. The project’s impacts are to make verification tools accessible to new user communities, address the urgent need for trustworthy AI-generated code in the maker and arts communities, and train students to be prepared for verification-focused engineering careers. The project advances educational research by exploring how formal reasoning can be taught through hands-on, project-based work and establishes a pipeline for future research into verification of AI-generated code for media arts software. Technically, the project develops new pedagogical strategies and tool integrations to introduce formal verification tools such as RTLola, TLA+, and Temporal Stream Logic (TSL) in creative contexts. The investigators adapt these tools to microcontroller-based platforms and design learning modules that align with the workflows of artists, designers, and creative coders. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.