Grothendieck (EGA I 0.7 & 1.10) defined a category of (topologically Noetherian) "formal rings" and a corresponding global category of formal schemes. Roughly, a formal ring is a topological commutative ring $R$ whose topology is $I$-adic for $I\subset R$ an open ideal. Its formal Spec is $Spf(R) : = Spec(R_{red})$ for $R_{red}$ the "maximal topologically reduced quotient", equivalently the reduced quotient of $R/I$. In the special case $I=0$ (discrete topology), we get the category of ordinary schemes as a full subcategory of formal schemes.
Given a formal ring $R$, we have a category $Mod(R)$ of suitably nice topological modules; these have a theory of completed tensor product and pullback. Again, this globalizes to a category of formal quasicoherent sheaves on a formal scheme.
Now in order to have pushforwards for formal sheaves, we need to allow new topological modules over ordinary rings. The fundamental example is the topological module $k[[t]]$ over $k[t]$ (the pushforward of the constant sheaf on the formal neighborhood of $0$). Since the completed stalk of $k[[t]]$ is zero at all points $0\neq x\in \mathbb{A}^1,$ it makes sense to think of this as a "formal sheaf on $\mathbb{A}^1$ supported at $0$".
I would like to understand a category of topological coherent sheaves on an ordinary scheme which includes such "formal" objects, and especially a derived category of such objects (I'm particularly interested in a category of "constructible" formal sheaves, which I would define as repeated extensions of pushforwards of coherent sheaves on formal completions of closed subschemes). For some reason, I can't seem to find anyone who has written about this, except for in the very general context of ind-schemes à la Gaitsgory-Rozenblyum. Do people here know of a good source?