Here's an example from distributed computing:
1 Background
1.1 Asynchronous Shared Memory Model
Let's consider a collection of distributed nodes that communicate using
shared memory variables. There is an adversary that controls when a node take steps
and when to deliver messages. The computation is asynchronous, i.e., the
adversary can delay the steps of nodes for any (finite) amount of time.
You can think of a step of a node as a state transition of its local
automaton (according to the algorithm) where the next state is determined
by the current state and the observations of the node since the last step.
1.2 Safety and Liveness
When formally reasoning about the properties of an asynchronous algorithm,
we distinguish between safety and liveness properties. Informally, a
safety property can be interpreted as a guarantee that something "bad"
never happens. (E.g., for mutual exclusion, a safety property would be
that no two nodes enter the critical section simultaneously.) Liveness,
on the other hand, can be interpreted as "something good will eventually
happen", e.g.: every node eventually terminates.
To formalize safety, we consider the infinite set ${M}$ of all possible
executions of all possible algorithms, taking into account all possible
choices of the adversary. An execution is an infinite sequence of steps. We can define a metric on $M$ by taking the distance between two distinct
runs $\alpha,\beta \in M$ to be $2^{-n}$ where $n$ is the first index where $\alpha$ and $\beta$ differ.
A safety property $S$ corresponds to some nonempty set $P\subseteq M$ that
is closed in the sense that the limit of an infinite
sequence of runs in $P$ cannot be in $M\setminus P$. So once we know that some property is a safety property, it is sufficient to show that this property holds on finite prefixes.
Applying Koenig's Infinity Lemma
It's not always straightforward to see whether a specific property is a
safety property: Consider the implementation of read/write atomic objects
on top of basic shared memory variables. Such an implementation should handle requests and their responses in a way that makes them look as if they happen at some instant in time and don't violate their order of invocation. (Due to the asynchronous operation, the actual duration between request and response might be nonzero.) Atomicity is also known as Linearizability. Section 13.1 of [A] gives a proof that Atomicity is a safety property. The proof uses Koenig's lemma to show that the limit of any infinite sequence of executions (each of which satisfies Atomicity) also satisfies Atomicity.
[A] N. Lynch. Distributed Algorithms. Morgan Kaufmann, 1996.
