Now I've gone and confused myself! I'm still fairly sure that the problem cannot be properly stated in formal terms, and yet I think I've figured out a solution. One of those has to be wrong. I'll present my suggested solution, then I'll go back and try to work out if I can see a way to formally state the problem.
When I say a solution, I mean an explanation of why they all have to wait until the 100th day, and what new information is provided at each stage. It turns out that new information becomes available every night when the ferry departs empty, and also on the Oracle's pronouncement on the first day (but not on subsequent days).
I shall use unary predicate C(r) to indicate u\geq r, where u is the number of blue-eyed people, and unary predicate K to indicate 'everybody knows that'. I will use indices to signify repeated applications of K. Thus K^3C(7) means
'Everybody knows that (Everybody knows that (Everybody knows that (u\geq 7)))'
Say there are n blue-eyed people (I'll call each such person a 'blue' from now on). It is not hard to show that we people with eyes of other colours do not affect the calculations, so we will omit them from consideration.
Then each person can see n-1 blues. So we have
$$KC(n-1)$$
A given person P entertains two possibilities, that u=n or u=n-1. In the second case, P will be non-blue, and what do they know about what others know? Each other person P' will be able to see (n-2) blues. On the other hand if u=n each other person P' will be able to see n-1 blues. So P knows that regardless of their own eye colour, each other person P' can see at least n-2 blues. That is, P knows that KC(n-2). Hence we have, since P is arbitrary:
$$K^2C(n-2)$$
Now think about what P knows about what another person P' knows. P knows it might be the case that P is non-blue and if so, for each other person P' it appears possible that P' is also non-blue. For P' considering that case they realize that each person P'' in the group excluding P' and P can see n-3 blues, so they know that u\geq n-3. For P' considering the alternative, where P' is blue, P'' can see n-2 blues. So either way P'' knows u\geq n-2. So P knows that P' knows that P'' knows that n\geq n-3. Whence we have:
$$K^3C(n-3)$$
We can continue this process, noting that at each step the exponent of K and the argument of C add to n.
So the initial state of knowledge of all players can be written as a vector of statements:
$$KC(n-1),\ K^2C(n-2),\ K^3C(n-3),\ ...\ ,\ K^{n-2}(2),\ K^{n-1}(1),\ K^n(0)$$
The ends are the easiest to interpret. The left says that everybody knows u\geq n-1 and the right says that everybody knows - ad infinitum - that there are at least zero blues.
Then the oracle speaks. Everybody hears her, and everybody knows that everybody else has heard her, so it is now the case that, for any natural number r, we have K^rC(1). This enables us to strengthen the last component of the knowledge vector by increasing the argument to C, but does not affect any of the other components. The new knowledge vector is:
$$KC(n-1),\ K^2C(n-2),\ K^3C(n-3),\ ...\ ,\ K^{n-2}(2),\ K^{n-1}(1),\ K^n(1)$$
So the oracle has communicated new information, not about what people know directly but about what they know others know others know others know...
Next, the ferry leaves and, if n>1 then nobody is on it. So now everybody knows that there are at least two blues, and they know that everybody else knows that, and they can prefix the K operator to that as many times as they like. The new knowledge vector is:
$$KC(n-1),\ K^2C(n-2),\ K^3C(n-3),\ ...\ ,\ K^{n-3}(3)\ ,\ K^{n-2}(2),\ K^{n-1}(2),\ K^n(2)$$
The next piece of new info is when the ferry leaves empty on day 2, provided n>2. Then everybody knows (to the umpteenth power) that u\geq 3. So the new knowledge vector is:
$$KC(n-1),\ K^2C(n-2),\ K^3C(n-3),\ ...\ ,\ K^{n-4}(4)\ ,\ K^{n-3}(3)\ ,\ K^{n-2}(3),\ K^{n-1}(3),\ K^n(3)$$
This continues, and each day the knowledge vector changes, by the minimum argument to all C predicates being increased by 1.
The general form of the knowledge vector after an empty ferry departure on day r is a vector of n components, of which the jth is:
$$K^{j}C(\max(n-j,r+1))$$
Each day, the knowledge of what others know others know increases, even though the direct knowledge of each person about the number of blues does not change.
When the ferry departs empty on day n-2 the knowledge vector has arguments with a minimum of n-1. Now, for the first time, everybody knows that everybody knows (etc, etc) that u\geq n-1. But they still don't know if their own eyes are blue. They only discover that when the ferry departs empty on day n-1 and the knowledge vector arguments attain a minimum of n. So, for all r we now have K^rC(n).
So they all leave on the nth day's ferry.
Every day there was new info from the ferry departure. And the first oracle pronouncement was necessary, although the subsequent ones were not.
