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 :-)