High-level requirements for a Proof of “Saving to the Database”

Question

This question is about a few sentence description of what a proof would look like (and technologies / logics involved) for a complex api call through many layers. Trying to get a sense of the techniques and key points to watch out for. I understand it would take a lot of work.

In learning about formal proof and verification, I've come across Operational Semantics, Hoare Logic, and Matching Reachability Logic. All of them are pretty low-level and describe how to prove stuff such as a while loop with a few assignment / arithmetic operations, but that's it.

I am wondering what the general / high-level requirements are to prove something like "saving a record through some https API to the database", where it goes through the network (https) and through a bunch of servers finally arriving at an array of replicated databases like MySQL.

In unit testing, you would simply write a test that the method (let's say save()) creates the record. You would make a database query and see if the record matched the record you thought it would be.

I am wondering what it would entail to write a proof of this (at a high level, just a few sentence description is all). What things would need to be proven. If you can't write a proof, then what if you still wanted to at least partially prove the system's correctness. What it would take.

It seems like you could write a Hoare Logic statement such as:

{P}
save({ type: 'asdf', foo: 'bar', a: 'b' })
{fetch('asdf', 'latest') == { type: 'asdf', foo: 'bar', a: 'b' }}

That's at least better than nothing. But I'm not sure if you can write a proof with just that.

Then to know that it actually was in the database and not in some cache in the browser, you would have to know that fetch had a proof that it went through the network to some API, and that API request went to the database, and the database did whatever. That's basically what I'm wondering, if creating a proof for save starts off with the Hoare Logic statement like above, and then progressively you add more detail to the proof. In this way it's almost developed like via TDD. At some point, then, I'm wondering when you could say "it is proven".