Yes? A huge portion of what a database does is amenable to formal methods. You can even come up with a reasonable rudimentary formal model of a physical machin

Yes? A huge portion of what a database does is amenable to formal methods. 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.)