On: Sqlite – Most Deployed Database in the World

[krylon]

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.

[monocasa → krylon]

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.

[krylon → monocasa]

Thanks, I did not know that.