Probably the same mechanism by which most proofs work, not fully formal but it seems to follow. Without the proofs in comments (or transitively through other asserts) it's up to the reader to recreate the argument, though. The purpose is to be more explicit than a comment, I suspect, using the same notation as the code.
sqlite has extremely thorough test coverage with something approaching 100% branch coverage and such wide production usage it's basically proven that a lot of this stuff works.