Huh, at that point it'd probably make more sense to formally verify it. For sel4 last time I checked the ratio was 25/1 proof code/verified code.

SQLite is used on many platforms, built using many compilers. All of those compilers might have bugs themselves (who am I kidding? They do), something verification cannot account for.

Sel4 takes the compiler out of the trusted computing base as well as well by verfying the binary directly.

Additionally, the majority of that test code is closed source, so it isn't getting run on nearly all the platforms sel4 supports anyway.

Thanks, I did not know that.

As far as I understand, formal verification does not certify the implementation even though the algorithms used are sound.

It depends—many proof-assistant languages let you extract an implementation directly out of your formally-specified algorithm (generally by dropping rich typing-ish information, but you've already verified it's correct). Or take seL4, which amazingly proves that not just the C code but also the binary faithfully matches their formally-specified algorithms. https://sel4.systems/Info/FAQ/proof.pml

Of course who knows what your CPU microcode is doing, but for the question at hand—ensuring a highly portable C library does what it claims to do more efficiently and accurately than exhaustive testing—formal verification is certainly a reasonable approach.