The main value from protocol level proofs is that since you need to tell the machine your assumptions before it spits out a proof, a careful proof development process can discover unstated assumptions.
The TLS Selfie attack is an example. In principle this attack could have been found during proof generation for TLS 1.3, but in practice the proofs generated during TLS 1.3 development smuggle in an unstated assumption that means Tamarin rules out Selfie even though in some cases it would be a viable attack.
[Selfie goes like this: Alice and Bob have a PSK for authentication, Mallory doesn't know the PSK, but Mallory can interfere with the network between Alice and Bob. Alice intends to ask Bob, "Do you have the car?". Mallory can't read this question or write an answer Alice will accept because they don't know the PSK. However, Mallory just redirects the question back to Alice. "Do you have the car?" and Alice doesn't have the car, so she answers "No" and she knows the PSK so her answer is proper. Now Alice gets an answer to her question, "No" and so she concludes Bob doesn't have the car. But actually Bob was never asked!]
Knowing about this, it can be repaired. Alice and Bob simply address the intended recipient in each message, "Bob, do you have the car?" "No Alice, I don't" - and check for their own name in messages they receive. Or they use a separate PSK for each direction, not just one per pair of participants in their system. Or they can choose only to either be a TLS client or a server and never both. But all these steps aren't obvious if there's nowhere stated the assumption that you did one of these three things. Intuitively it seems as though since Mallory doesn't know the PSK and the Tamarin prover says this protocol works you're fine.