I got this problem from Rustan Leino, who got it from Jay Misra, who had received it from Edsger Dijkstra. This particular description of the problem borrows from a description given by Michael Jackson.
I solved it and wrote up my solution.
In a finite, undirected, connected graph, an integer variable $v(n)$ is associated with each node $n$. One node is distinguished as the anchor. An operation $\mathsf{OP}(n)$ is defined on nodes, as follows.
$\mathsf{OP}(n)$: If node $n$ is the anchor, then do nothing; otherwise, set $v(n)$ to the value $1 + \mbox{min}\{v(m)\},$ where $m$ ranges over all neighbors of $n$ that are distinct from $n.$
An infinite sequence of operations $\langle \mathsf{OP}(n), \mathsf{OP}(m), \ldots \rangle$ is executed, the node arguments $n$, $m$, ... for the operations being chosen arbitrarily and not necessarily fairly. Show that eventually all $v(n)$ stabilize. That is, that after some finite prefix of the infinite sequence of operations, no further operation changes $v(n)$ for any node $n.$
We say that a node $n$ is visited by an operation when the operation is $\mathsf{OP}(n)$. We call a node $n$ stable if its variable $v(n)$ changes a finite number of times, and unstable otherwise.
Let $\cal S$ be the set of stable nodes, and $\cal U$ be the set of unstable nodes. Clearly, $\cal S$ is non-empty, since it contains the anchor. We want to prove that $\cal U$ is empty, so for the sake of contradiction let's assume it's non-empty.
Let ${\cal S}_\mbox{adj}$ be the set of stable nodes that are adjacent to at least one unstable node. This set must be non-empty since otherwise the graph is disconnected.
Since the graph is finite, ${\cal S}_\mbox{adj}$ is finite. Thus, nodes in this set change their variables a finite number of times. Thus, there must be some operation number $t_0$ after which no node in ${\cal S}_\mbox{adj}$ ever changes its variable. For any $s \in {\cal S}_\mbox{adj}$, define $v_\mbox{final}(s)$ to be its variable value after operation number $t_0$.
Let $s_\mbox{min}$ be any $s \in {\cal S}_\mbox{adj}$ that minimizes $v_\mbox{final}(s)$. Such an $s$ must exist because ${\cal S}_\mbox{adj}$ is finite and non-empty.
Define $\cal A = {\cal S}_\mbox{adj} \cup {\cal U}.$ We use the letter $\cal A$ to connote adjacency, since every neighbor of an unstable node is in $\cal A$.
Let the variable $\mathsf{MinA}$ represent $\mbox{min}\{v(a) \mid a \in {\cal A}\}$. This is well-defined since $\cal U$, and thus $\cal A$, is non-empty.
Lemma 1. At any point after operation number $t_0$ (not necessarily immediately after that operation), whenever $\mathsf{MinA}$ equals $q$ it will forever after be $\geq q$.
Proof. Suppose not. Then, there must be some operation that makes $\mathsf{MinA}$ go from $\geq q$ to $< q$. This operation must be some $\mathsf{OP}(n)$ that sets $v(n) < q$ for some $n \in {\cal A}$. Since it's after $t_0$, nodes in ${\cal S}_\mbox{adj}$ have stopped changing, so $n$ must be in $\cal U$. This means all its neighbors are in $\cal A$. This means that, immediately before the operation, all its neighbors $m$ had variables $v(m) \geq \mathsf{MinA} \geq q$. Thus, the operation sets $v(m)$ to some number $\geq q+1$. This contradicts it setting $v(n) < q.$ This contradiction completes the proof.
Lemma 2. At any point after operation number $t_0$ (not necessarily immediately after that operation), whenever $\mathsf{MinA}$ equals $q$ where $q < v_\mbox{final}(s_\mbox{min})$, $\mathsf{MinA}$ will eventually be $> q$.
Proof. Suppose it's after operation number $t_0$ and $\mathsf{MinA} = q < v_\mbox{final}(s_\mbox{min})$. By Lemma 1, $\mathsf{MinA}$ will forever after be $\geq q$. Thus, every time we have an $\mathsf{OP}(u)$ on an unstable node $u$, all its neighbors $m$ will have $v(m) \geq q$ and the operation will set $v(u) > q$. Since all unstable nodes change infinitely often, they will all eventually be visited by an operation that sets them to $> q$. Furthermore, they'll remain $> q$ because all subsequent operations also set them to $> q$. Thus, eventually all unstable nodes will have variables $> q$. Since we're after operation $t_0$, all nodes in ${\cal S}_\mbox{adj}$ remain unchanged with values $\geq v_\mbox{final}(s_\mbox{min})$. This is also $> q$. Thus, eventually all nodes in ${\cal A}$ have variables $> q$, and $\mathsf{MinA}$ exceeds $q$.
A consequence of Lemma 2 is that, after operation $t_0$, $\mathsf{MinA}$ will eventually be $\geq v_\mbox{final}(s_\mbox{min})$. Call $t_1$ the operation number when this happens. By Lemma 1, from then on $\mathsf{MinA}$ will always be $\geq v_\mbox{final}(s_\mbox{min})$.
By definition of ${\cal S}_\mbox{adj}$, each node in it, including $s_\mbox{min}$, is adjacent to at least one unstable node. Let $u_\mbox{adj}$ be an unstable node adjacent to $s_\mbox{min}$.
After operation number $t_1$, every time $u_\mbox{adj}$ is visited, it finds the following. All its neighbors $m$ are in $\cal A$ and thus have variables $v(m) \geq v_\mbox{final}(s_\mbox{min}).$ One of its neighbors, namely $s_\mbox{min}$, has variable $v(s_\mbox{min}) = v_\mbox{final}(s_\mbox{min})$. Thus, the minimum $v(m)$ among its neighbors equals $v_\mbox{final}(s_\mbox{min})$. This means that the operation sets $v(u_\mbox{adj})$ to be $v_\mbox{final}(s_\mbox{min}) + 1$.
This means that the node $u_\mbox{adj}$ can change its variable at most once more, to $v_\mbox{final}(s_\mbox{min}) + 1$, because every time it's visited its variable is set to this identical value. This means that $u_\mbox{adj}$ is stable, since it changes a finite number of times. This contradicts the definition of $u_\mbox{adj}$, and this contradiction falsifies our assumption that $\cal U$ is non-empty.
Since $\cal U$ is empty, all nodes are stable, and thus every node changes its variable a finite number of times. Thus, there must be some operation number after which no node $n$ ever changes its $v(n)$. This completes the proof.