Possibly this question is bit too broad but up to now I was not able to find a satisfying answer.

Let $X$ be a locally Noetherian scheme and $X' \subset X$ be a closed subscheme of $X$ which is defined by an ideal $\mathcal{I} \subset \mathcal{O}_X$. Again one denotes $X_n = Spec\mathcal{O}_X/\mathcal{I}_{n+1}$ and obtains a chain of thinkening $X_• = (X_0 \to X_1 \to ...)$. Taking the colimit of $X_•$ we get a formal scheme $\hat{X}$ where $|\hat{X}| = |X'|$ and $\mathcal{O}_{\hat{X}} = \varprojlim_n \mathcal{O}_{X_n}$, also called the formal completion of $X$ wrt $X'$. My main reference is Doan Trung Cuong's excellent Minicourse.

My question is simply where in algebraic geometry this concept of formal schemes used in a fruitful way. The only "big" theorem that I know based on this concept is the "** Theorem on formal functions**".

Remark: By "fruitful" I mean that we can make usage of this theory as "new" toolbox in order to obtain new conclusions about schemes in "common" sense (note that formal schemes are ringed spaces and not schemes in usual sense). An excellent prototype of such interplay with the concept of formal schemes is again Theorem on formal functions, as we can deduce from it for example the Stein factorisation, a variant of Zariski main theorem.

Again, unfortunatelly up to now during my research the TofF was the only "big" result that is provided by this formalism. Are there more such notable results of similar caliber?

What is the philosophy of taking formal completions of usual schemes? Or what is the motivation, so which kind of "new" information about the scheme one intends to find out applying concept, which seems be not extractable without it?