Hi Andrej, I left this open for a few months in the hopes that someone could answer my original question, but given the silence I take it that the answer is in fact "No, no one's looked at this since." So I'm going to accept your excellent answer. As you say, this sounds like a nice little research project.

Would the absence of LEM be more problematic than it already is in constructive reverse maths?

By Löb's theorem, if $ZFC \vdash Bew(\ulcorner\varphi\urcorner) \rightarrow \varphi$ then $ZFC \vdash \varphi$.

@FredRohrer according to Mathias, replacement did not appear in the older editions of Bourbaki, but was added later. dpmms.cam.ac.uk/~ardm/bourbaki.pdf

I don't know that anyone currently defends a position like this. In the mathematical and philosophical literature on reflection principles people are certainly aware of Reinhardt's work, but most current work eschews the idea of extending $V$.