I just thought of a new proof that is for free using modern technology. It resembles the first step of the other proof, but replacing the sheaf of differentials with the cotangent complex.
In order to see that the map $f:R\to S$ is formally étale, it will be enough to show that the entire cotangent complex vanishes. The property of a (derived) module being zero can be tested on stalks, so it suffices to show that the stalk of the cotangent complex $\mathbb{L}_{S/R}$ at each prime $\mathfrak{p}\in \operatorname{Spec}(S)$ vanishes, that is to say $$\mathbb{L}_{S/R}\otimes^\mathsf{L}_S S_\mathfrak{p}=0$$ for all primes $\mathfrak{p}\in \operatorname{Spec}(S)$
Suppose $f:R\to S$ such that for every prime $\mathfrak{p}\in \operatorname{Spec}(S),$ we have that the cotangent complex of the composite map $R\to S\to S_\mathfrak{p}$ vanishes, that is to say, $\mathbb{L}_{S_\mathfrak{p}/R}=0$.
But we have a fibre sequence:
$$\mathbb{L}_{S/R}\otimes^\mathsf{L}_S S_\mathfrak{p}\to \mathbb{L}_{S_\mathfrak{p}/R}\to \mathbb{L}_{S_\mathfrak{p}/S}.$$
However, the cotangent complex $\mathbb{L}_{S_\mathfrak{p}/S}$ vanishes because the localization at a prime is a filtered colimit of localizations, which makes it formally étale. Ergo, we have an equivalence of derived modules
$$\mathbb{L}_{S/R}\otimes^\mathsf{L}_S S_\mathfrak{p}\xrightarrow{\sim} \mathbb{L}_{S_\mathfrak{p}/R},$$
but by assumption, $\mathbb{L}_{S_\mathfrak{p}/R}=0,$ so it follows that
$$\mathbb{L}_{S/R}\otimes^\mathsf{L}_S S_\mathfrak{p}=0,$$
as desired.