If you’re not a computer scientist, skip this post. The biggest impediment to formal verification of systems code is currently this: we have at least three extant formal semantics for C, no viable formal semantics for Rust, and no other viable systems languages. (Yes, I am ignoring C++.) If we want to formally verify systems code at all, never mind at scale, we need either a new systems language with a formal semantics, or we need a formal semantics for Rust and a reasonable feeling that the semantics reflects the actual implementation of the language and can be maintained going forward as the language evolves. Unfortunately, as good as Rust is, and it is very good by historical standards, it is a complicated language, and there is a strong suspicion that the type system is not actually sound. It is also probably too large a language for which to build a formally verified compiler given the current state of the art (though that might change), and it is not clear that the official compiler would not rapidly evolve away from a version of the language that a formally verified compiler implemented. Even given a formally verified compiler and a semantics, neither of which exist, the current proof assistant landscape, tools like Rocq and Lean, are hardly ideal for this sort of work, even given AI assistance. So, we are in a position in which we know that there is a substantial gap between what we need in order to move forward to formally verified systems software, and the tooling that we have currently. This is a hard problem. It is also one that needs a solution, or more likely, a set of solutions. (One irony of the current situation is that most experiments in formally verified systems software still reuse one of CompCert’s intermediate representations as a target. And thus, C is still being perpetuated, even in high assurance programming work.)