Through then it also seems that many of the newer bugs sl seem to be around more advanced features which sometimes can be disabled on compiler time. (newer=after they integrated fuzzing into their tested)

I wonder if it makes sense for Oses to ship two versions of sqlite one for the small local "trusted" database case and one for the sqlite as file format case which had many features disabled, only allowing the core subset of sqlite.

Through if you provide some "evergreen" software you can anyway just include your own version of sqlite. Potentially statically linked in.

You can even come up with a reasonable rudimentary formal model of a physical machine/CPU and check against that. Sure, the model of the machine may be wrong in subtle ways, but when you discover that, you fix it and recheck your model of a database against the updated model of a physical machine.

That said... don't use a language with trivially allows for out-of-bounds indexing, etc. (SQLite was started when there were really few other good options, so that's understandable.)