Xavier Leroy

Maybe, but on the other hand maybe the CakeML developers have some proof techniques that the CompCert people didn't think of. I don't know.

For reference, my only knowledge of this point comes from the CC 2010 paper at https://xavierleroy.org/publi/validation-regalloc.pdf, which says in section 5: "From a proof engineering viewpoint, the validator is a success. Its mechanized
proof of correctness is only 900 lines of Coq, which is quite small for a 350-line piece of code. (The typical ratio for Coq program proofs is 6 to 8 lines of proof
per line of code.) In contrast, 4300 lines of Coq proof were needed to verify
the register allocation and spilling passes of the original CompCert compiler.
Even this earlier development used translation validation on a sub-problem: the
George-Appel graph coloring algorithm was implemented directly in untrusted
Caml code, then followed by a verified validator to check that the resulting as-
signment is a valid coloring of the interference graph. Later, Blazy, Robillard
and Appel conducted a Coq proof of the graph coloring algorithm [13]. This is
a fairly large proof: in total, more than 10000 lines of proof are needed to com-
pletely verify the original CompCert register allocation and spilling passes."

(And hence my statement above was also inaccurate in that the original CompCert was not fully directly proven. I had misremembered the details of this paragraph. The point still stands that the newer…

I didn't touch on that, but I did assume trust of the Rust toolchain, verifying starting at THIR. Verifying rustc would be a monumental undertaking, though I think some people are working on it.

Since we don't have a verified rustc (a la CompCert [0]), I wonder if an approach like the translation validation of seL4 [1] would work. They prove that the artifact (ARM machine code) produced by an existing compiler (gcc) for a chosen program (seL4) matches the source semantics (C). Thus you could circumvent trusting rustc, but it only works to verify a specific output of a chosen program. If the chosen program was coq-of-rust, I don't think this would be easier than the approach I detailed above. The seL4 kernel is 9,500 lines of C, while their Isabel/HOL specification is over 200,000 lines, so the technique doesn't seem to scale to a large chosen source like rustc.

Isn't bootstrapping fun?

[0]: Xavier Leroy. 2008. “Formal verification of a realistic compiler”. https://xavierleroy.org/publi/compcert-CACM.pdf

[1]: Thomas Sewell, Magnus Myreen, and Gerwin Klein. PLDI 2013. “Translation Validation for a Verified OS Kernel”. https://sci-hub.st/10.1145/2491956.2462183

That's just start.

The bleeding edge uses abstract interpretation to verify code.

Free from NASA: IKOS (Inference Kernel for Open Static Analyzers) is a static analyzer for C/C++ based on the theory of Abstract Interpretation. https://github.com/NASA-SW-VnV/ikos

Commercial: Astrée is a static analyzer for safety-critical software written or gen­er­ated in C or C++. https://www.absint.com/astree/index.htm https://www.absint.com/astree/index.htm

abstract interpretation for static analysis and verification:

Good intro Mechanized semantics, fifth lecture Abstract art: static analysis by abstract interpretation https://xavierleroy.org/CdF/2019-2020/5.pdf

Static Analysis and Verification of Aerospace Software by Abstract Interpretation https://mine.perso.lip6.fr/publi/article-bertrane-al-fntpl15.pdf

Historically, smartcard chips were very underpowered 16- or even 8-bit MCUs that couldn't even perform Java bytecode validation on-chip (which caused some security vulnerabilities in the past; there's interesting academic literature on this if you're curious, for just one example see [1]).

These days, these are sometimes ARM M0 cores which are significantly more powerful. I think Doom over SAT (SIM application toolkit) is within reach :)

[1] https://xavierleroy.org/publi/oncard-verifier-spe.pdf