Critical embedded systems deserve the highest level of assurance to guarantee that their implementation satisfies their specification. Verification techniques such as proof by deduction operate at source level but the verification effort often requires to design higher-level abstractions that facilitate the reasoning. However, this approach comes at the cost of assuming the correctness of the abstraction with respect to the source code.

To circumvent this problem, we have defined a verification-aware DSL designed to program and prove critical embedded software. Our DSL, named Barocq, is minimal and purely functional. It makes programs amenable to verification inside the Rocq proof-assistant. Barocq comes with a compiler to C that generates efficient and human-readable programs. Barocq bridges the gap between the program that is reasoned about and the program that is compiled. A key feature of Barocq is that its semantics and data-representation are zero-cost abstractions at runtime. This is achieved by enforcing, using static analysis, a strict alias-control programming discipline which enables to compile functional updates as imperative in-place mutations and minimise pointer dereferences using unboxed data-structures.

Finally, we demonstrate that Barocq has the adequate features to write an interesting class of critical embedded code, including most components of the S3K microkernel, which can be used as drop-in replacement of the original C code.