High-level requirements for a Proof of "Saving to the Database"
The SoftwareEngineering.SE link gives the wrong answer for the right reasons. You can only ever prove anything with respect to a formal model. Verifying that that formal model accurately captures reality (or at least accurately captures the parts you care about for your purposes) is an informal process. In many applications of formal methods, one of the most time consuming and difficult parts is creating and validating the formal model. For example, for the CompCert project they had to make both a formal model for the behavior of C and a formal model for the behavior of the target processor (at least for the instructions they use). Both of these are massive undertakings on their own. 

It makes no sense to "add more detail to the proof". Either a statement has a proof or it doesn't. It's proven if it has a proof. All proofs are equivalent for this purpose. What you can add more detail to is the formal model. Except "add more detail to" has the wrong connotations. You generally want the least detailed model that is accurate and for which you can prove your desired properties, e.g. correctness. The only reasons to change to a more detailed model is 1) you can't actually prove what you want with the original model, 2) the original model is wrong in which case your new model is not compatible with it, or 3) which is really a variant of (1), there is a different program that you could write that exploits those details to achieve the same functional behavior but different non-functional properties such as performance or implementation simplicity. In all these cases we need a new proof because we've changed the statement we're proving: either by changing the program or by changing the assumptions.

There are two aspects to the use of a formal model. First, as far as your program is concerned, it doesn't care if the database saves the data or even if the database exists. It only cares that the operations it uses behave as specified with respect to a given formal model. That formal model can be very high-level and abstract with no reference to any notion of "database" or "network" or "HTTP". However, it will likely be quite complicated to soundly capture the realities of the actual underlying systems. Second, at the systems level, you certainly do care whether the data was committed to the database as opposed to just being stored in some local cache. At the level of the program, there is absolutely no way for you to guarantee this. Your program could always be running in a sandbox that mimics any observable behavior. All you can prove at the program level is that your program will invoke some sequence of operations that putatively will lead to data being committed to the database. At some point you just have to accept based on empirical evidence that the chosen real world implementation faithfully implements the formal model. You can provide an implementation of the primitives of a high-level model with respect to a lower-level formal model that has been proven correct if you want to reduce how much you need to accept without (mathematical) proof.

The current state of play is that most programming languages lack publically available, normative (mechanized!) formal models let alone the underlying hardware. Ipso facto, most standard libraries, applications, operating systems, drivers, etc. are not proven correct since they have nothing with respect to prove their correctness. This is both in the sense that there isn't a formal model of what "correct" even means, nor is there a formal model of the implementation language so that you know what the implementations even do. In other words, in most cases we neither know what an implementation does nor what we even want it to do. This is why the artifacts (and tooling) produced by the CompCert projects and its related projects and by the $\mathbb K$ framework folks and several other groups are so important. Without these artifacts, you either use some massively over-simplified and weakly verified formal model that implicitly assumes millions of lines of codes are "correct" (spoiler: they aren't)1, or you invest man-centuries building a chain of trust. With luck, in the near-ish future some critical mass of formalization will be reached and proving the correctness of your program will become proportional to the complexity of your program and not the entire ecosystem.

1 While using an oversimplified formal model doesn't provide most of the benefits of "provable correctness", it does, in practice, do an excellent job of improving code quality by revealing mistaken assumptions in the code. Of course, the mistaken assumptions in your formal model have to be detected the old-fashioned way for the most part.