Formal verification is a promising approach to eliminate bugs at compile time, before they ship. Indeed, our community has verified a wide variety of system software. However, much of this success has required heroic developer effort, relied on bespoke logics for individual domains, or sacrificed expressiveness for powerful proof automation.

This work previews the MilSpec suite, a diverse collection of benchmarks targeting heterogeneous embedded/edge systems. These end-to-end and kernel-level benchmarks are inspired by defense-related applications and applicable to the broader system design space. They exercise a wide range of computational capabilities, such as signal processing, image processing/computer vision, and matrix-based computation, which are particularly relevant for modern embedded applications that must process large amounts of data at the edge.