Given the central role that C continues to play in systems software, and the difficulty of writing safe and correct C code, it remains a grand challenge to develop effective formal methods for verifying C programs. In this paper, we propose a new approach to this problem: a type system we call \textbf{RefinedC}, which combines \emph{ownership types} (for modular reasoning about shared state and concurrency) with \emph{refinement types} (for encoding precise invariants on C data types and Hoare-style specifications for C functions).

RefinedC is both \emph{automated} (requiring minimal user intervention) and \emph{foundational} (producing a proof of program correctness in Coq), while at the same time handling a range of low-level programming idioms such as pointer arithmetic. In particular, following the approach of RustBelt, the soundness of the RefinedC type system is justified semantically by interpretation into the Coq-based Iris framework for higher-order concurrent separation logic. However, the typing rules of RefinedC are also designed to be encodable in a new “separation logic programming” language we call \textbf{Lithium}. By restricting to a carefully chosen (yet still expressive) fragment of separation logic, Lithium supports predictable, automatic, goal-directed proof search \emph{without backtracking}. We demonstrate the effectiveness of RefinedC on a range of representative examples of idiomatic C code.