Most interesting to me is that it's implemented in a language I'd never heard of, F* (https://www.fstar-lang.org/), which is an ML that compiles to OCaml, F#, or a subset of the language can compile to C. It's intended for just this sort of work ("verified effectful programming" is seemingly one of their taglines for the thing).

That's pretty neat. I like seeing exotic languages used in mainstream projects. It's just fun, ya know? Firefox is also shipping with some Rust code these days.