One might be able to formally verify the sqlite pager layer, where this problem occurred. It's just writing pages to disk and reading pages from disk, and providing ACID guarantees.