I think the docs cover this. They assume on purpose that the program never touches a proxy, so the proof only holds if that's true. To me that's the more interesting thing to argue about, what the proof assumes, not whether the author knows TS is unsound.