I don't really know of more on the issue as I haven't looked at his two recent elliptic papers in much depth yet, but I still don't think more has been formalized. I gather there's enough in there that one could probably write down equivariant elliptic cohomology over Z if one wished, although I don't think that has actually been done formally

and I'm not sure how to go beyond that to 2-equivariance (although I imagine that if you admit the `hack' of allowing some knowledge of what the 2-groups actually are, you might be able to similarly use his last two papers to define the appropriate twists directly again)

@ArnavTripathy weird situation. I'll check back in another decade

@ArnavTripathy @pupshaw Lurie doesn't talk about equivariance or higher equivariance in the two Elliptic papers that are out.

I'm sure the discussion in Elliptic-I about biextensions is very relevant to the construction of the canonical symmetric biextension over $M_{\mathrm{Ell}}^{\mathrm{or}}$ discussed at the end of Survey 5.1, but I don't see symmetric biextensions discussed in Elliptic-I or a discussion of how to describe them in a way which leads to 2-equivariant cohomology.

(E.g., that symmetric biextensions are basically the same as certain kinds of functors $\mathcal{C}\to \mathrm{SpDM}$, where $\mathcal{C}$ is a suitable category. Here $\mathcal{C}$ is probably something like the full subcategory of $\infty$-groupoids with $\pi_2$ and $\pi_3$ free and finitely generated, and all other $\pi_k=0$.)

(Once you have that, it shouldn't be too hard to construct a 2-equivariant cohomology theory.)