Right. The paper notes that they stubbed out all the trickier crypto and system call routines with contracts. If those routines don't adhere to the modeled contracts in real execution, then the proof's guarantee won't hold. Also things like concurrency and signal handling are intentionally not modeled.

I think this is an incredible result and I hope we'll see more and more of it, but even still, it's verifying a pretty thin slice of an actually executing system!