Applications of Koszul's formula other than the fundamental lemma of Riemannian geometry I'm wondering what else one can do with Koszul's formula
$$2\langle\nabla_XA,B\rangle = X\langle A,B\rangle-B\langle X,A\rangle + A\langle X,B\rangle - \langle A,[X,B]\rangle + \langle[B,X],A\rangle - \langle B,[A,X]\rangle$$
beyond proving existence and uniqueness of the Levi-Civita connection. I haven't yet seen anybody using it for anything else, which would be quite curious.
Here's a pretty and simple example. I don't know if it is known...
Let $\nabla^{LC}$ be the Levi-Civita connection and $\nabla$ be some other metric connection with torsion $T$. Then
$$2\langle\nabla_XA,B\rangle - 2\langle\nabla_X^{LC}A,B\rangle= \langle T(A,X),B\rangle -\langle T(A,B),X\rangle - \langle T(B,X),A\rangle$$
An application of this would be to compute the LC-connection for the metric $\langle K\cdot,K\cdot\rangle$ in terms of the endomorphism $K$ and the LC-connection for $\langle \cdot,\cdot\rangle$. The computation starts with the connection $K^{-1}\nabla^{LC} K$, which is metric for $\langle K\cdot,K\cdot\rangle$...
I can't guarantee correct letters and signs :-)
 A: Koszul's formula simply expresses the Levi-Civita connection explicitly in terms of the Riemannian metric. It is quite useful any time you want to eliminate the connection from a formula and write the formula in terms of the metric only. José cited some nice examples. I haven't checked, but I bet the book by Cheeger and Ebin discusses these examples and maybe  more quite explicitly.
But it is no different from writing a formula in local co-ordinates and replacing all appearances of Christoffel symbols by their formula in terms of partial derivatives of the Riemannian metric. This is often an equally useful thing to do when, for example, you want to apply PDE techniques or theorems that are stated in terms of co-ordinates to a problem in Riemannian geometry.
A: I've meanwhile found out that my innocent example ...
1.) ... amounts to a rediscovery of Schouten's contorsion tensor. (See e.g. this note). This concept is important in torsion gravity (which isn't as exotic as it may sound - except for some charlatanry derived from it...) My example equation seems to express the equivalence principle (cf. link eq. (255)). See also Rodrigues & Oliveira: The many faces of Maxwell, Dirac and Einstein equations.
As I've already hinted here, contorsion stuff (or what I would term the contorsion operator) can also occur in computations with torsion-free connections.

2.) ... leads to a generalization of the fundamental "lemma", a.k.a. Levi-Civita theorem: For any given vector-valued 2-form $T$ there exists a unique metric connection with torsion $T$.
