This amount of nontrivial, yes. Similarly, I'd expect a computer scientist to come up with a proof of correctness for either binary search or merge sort (the out of place variant) in ~30 minutes. It's not particularly difficult.
The number of incorrect binary search algorithms published in the literature over the years would indicate otherwise…
I agree that reasoning about the correctness of a binary search algorithm is an important job skill for a computer scientist. Deriving the tortoise and hare algorithm on the fly, though, is not.