Say $X$ is a smooth projective variety and $\beta\in H_2(X)$ is a class. Then there is a finite-type proper scheme $SM : = \overline{\mathcal{M}}_{g,n}(X,\beta)$ of stable maps to $X$ from nodal curves of genus $g$ with $n$ marked points in $X$ with class $\beta$. Famously, this scheme has a "virtual fundamental class" which is often nowhere close to the fundamental class of $SM$ (which may be highly singular and of the "wrong" dimension). However, it is now an accepted fact that the scheme $SM$ has a derived thickening, $\widetilde{SM},$ which correctly captures the "intersection-theoretic" meaning of $SM$ and has the appropriate virtual fundamental class.

All the constructions of such a scheme that I found seem complicated: they involve obstruction theory, deformation to the normal curve, etc. However there seems to me a very straightforward construction using formal intersection theory which has probably been considered by many people, but I have not found it written down. I suspect there is some reason why it does not work or requires too much new technology.

Namely, say $f:C\to X$ is a stable map, and $C = U_1\cup U_2$ is a cover of $C$ by two affines. Let $U_{12}$ be their intersection. For any affine curve, $Map(U, X)$ is a smooth infinite-dimensional formal (ind-) variety. Now consider the derived intersection in a formal-geometric sense $$Map(U_1,X)\times^L_{Map(U_{12}, X)} Map(U_2, X).$$ This is a smooth derived scheme whose underlying classical scheme is a subscheme of $Map(C, X)$, and it can be seen (at least in a neighborhood of the map $f:C\to X$) to be locally of finite type (i.e. there is some half-infinite intersection business going on). It seems that this procedure can be performed "consistently" for every fiber of $SM$ (possibly involving some patching), and this should be the "correct" derived intersection-theoretic meaning for the moduli of stable maps.

Are there difficulties in using this technique? Why doesn't it seem to exist in the literature?