Uses the Lean theorem prover from Microsoft that was designed to work with real-world code with higher automation than what’s typical in proof assistants. They’re aiming at SPARK or Frama-C more than Coq. The embedded subset is actually larger than I saw for some of the automated work in C which basically reduces down to expressions, while loops, and some heap stuff. So, such an approach might already be useful by itself given a fraction of it was useful for C code esp in embedded.
This could lead to some very solid libraries – HTTP parsers, crypto, JSON parsers, regular expressions – with verified safety and verified runtimes (asymptotic complexity).