Restriction to the formal neighbourhood Let $\pi: X \to Y$ be a proper map of schemes over an algebraically closed field $k$ and let $F$ be a coherent sheaf on $X$. Let $y \in Y$ be a closed point. I want to understand the pullback of $R^i \pi_* F$ along the natural map $\operatorname{Spec} \hat{\mathcal{O}_{Y, y}} \to Y.$
Is it the same as just the completion of $R^i \pi_* F$ at $y$? Or is there any nice interpretation of this pullback?
 A: I misread what you originally asked. What you are asking about is much more elementary.
Namely, observe that as $\pi$ is proper that $R^i\pi_\ast F$ is a coherent $\mathcal{O}_Y$-module, and so if we pull this back along $\mathrm{Spec}(\widehat{\mathcal{O}}_{Y,y})\to Y$ we get some finitely generated $\widehat{\mathcal{O}}_{Y,y}$-module $M$. On the other hand, by the completion of $R^i\pi_\ast F$ at $y$ you mean the complete $\widehat{\mathcal{O}}_{Y,y}$-module given by $\varprojlim M_n$ where $M_n$ is the $\mathcal{O}_{Y,y}/\mathfrak{m}_y^n$-module you obtain by pulling back $R^i\pi_\ast F$ along $\mathrm{Spec}(\mathcal{O}_{Y,y}/\mathfrak{m}_y^n)\to Y$. Let us observe that, essentially by definition, we have that $M_n=M/\mathfrak{m}_y^n M$, and so we see that have reduced the question to whether $M$ is $\mathfrak{m}_y$-adically complete. But, this is classical.

Proposition 1: Let $R$ be a Noetherian ring complete with respect to an ideal $J$. Then, any finitely generated $R$-module $M$ is $J$-adically complete.

----- Below is a tangent that I just find interesting, feel free to ignore -----
In fact, more is true. Fix $A$ to be a ring complete with respect to a finitely generated ideal $I$. By [FK, Chapter 0, Corollary 7.4.7] for a finitely generated $A$-module $M$, being complete is equivalent to being separated. What guarantees separatedness? One possible answer is actually interesting.

Definition: Let us say that $I$ satisfies the $\textbf{(APf)}$ property if for any finitely generated $A$-module $M$ and any finitely generated submodule $N\subseteq M$, the $I$-adic topology on $N$ and the subspace topology on $M$ coincide. Equivalently, if for any $n\geqslant 0$ there exists an $m\geqslant 0$ such that $N\cap I^m M\subseteq I^nN$.

We then have the following.

Proposition 2 ([FK, Chapter 0, Corollary 7.4.17]): Suppose that $I$ satisfies the $\textbf{(APf)}$ condition. Then, any finitely generated $A$-module is $I$-adically complete.

Proposition 1 is a special case of Proposition 2 since $J$ automatically satisfies the $\textbf{(APf)}$-condition by the Artin--Reese lemma. But, it holds more generally. Namely, say that the pair $(A,I)$ is Noetherian outside $I$ if $\mathrm{Spec}(A)-V(I)$ is a Noetherian scheme. Then, a beautiful theorem of Gabber (see [FK, Chapter 0, Theorem 8.2.19]) says that $I$ automatically satisfies $\textbf{(APf)}$ (and much more)!
Of course, this gives another (somewhat perverse) proof of Proposition 1 via Proposition 2 (without directly mentioning Artin--Reese) as evidently if $A$ is Noetherian the $(A,I)$ is Noetherian outside $I$.
To see why this is of interest beyond that, note that you can apply this theory to rings that come up in other areas of arithmetic geometry. For instance, it applies to the ring $\mathcal{O}_{\mathbb{C}_p}\langle t\rangle$ where $\mathbb{C}_p$ are the $p$-adic complex numbers, and this ring is defined as the $p$-adic completion of $\mathcal{O}_{\mathbb{C}_p}[t]$. Indeed, while this ring is patently non-Noetherian, it is Noetherian outside $(p)$, as is well-known from rigid geometry (e.g. see [FK, Chapter 0, Proposition 9.3.2]).
Fun bonus exercise: Do you need to assume anything about the pair $(A,I)$ for a finitely generated projective $A$-module to be complete?
References:
[FK] Fujiwara, K. and Kato, F., 2018. Foundations of rigid geometry. European Mathematical Society.
