Formal Schemes Methods: Applications 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?
 A: Instead of trying to answer the question in full, let me give some further appearances of the notion of formal scheme.


*

*There are several situations when a consideration of a topology in certain rings makes the situation simpler, e.g. every complete regular noetherian algebra over a field is a ring of power series, therefore infinitesimal neighborhoods makes clear certain features of a geometric problem that in the usual context is hidden. This is in line with Zariski's philosophy of "algebraic holomorphic functions". For example, to define algebraic residues one needs to complete, and in the complete setting, the duality between local cohomology and derived completion plays a certain role.

*In certain circumstances you can restore non singularity by completing. Let $X$ be a projective variety over a field of characteristic 0. If you complete the ambient projective space along $X$ you obtain a formal scheme that is smooth (in an appropriate sense) over the base field and whose De Rham cohomology corresponds to the singular cohology of the underlying space of $X$ if the base field is $\mathbb{C}$. This is the philosophy of De Rham cohomology of algebraic varieties as developed by Hartshorne. See:
Hartshorne, Robin: On the De Rham cohomology of algebraic varieties. Publ. Math. IHES No. 45 (1975), 5–99.  


*There is a further trait, that is the use of formal schemes as algebraic models of rigid analytic varieties over a complete valued field. To begin, look at:


Lütkebohmert, Werner: Formal-algebraic and rigid-analytic geometry. Math. Ann. 286 (1990), no. 1-3, 341–371.


*Formal schemes show up quite naturally in the context of Lefschetz theory, i.e. the reconstruction of properties of an algebraic variety by knowing properties of its hyperplane sections. 
See (especially chapters IV and V):


Hartshorne, Robin: Ample subvarieties of algebraic varieties. Lecture Notes in Mathematics, Vol. 156 Springer-Verlag, Berlin-New York, 1970.
This a sample of some different context where formal schemes arise. Sometimes a topology allows to tame a situation where non-finitely generated algebras arise.
For some reason, there are few systematic development of the main properties of formal schemes but their uses are pervasive in algebraic geometry. Hope my pointers help.
