Constructible-level absoluteness over ZF ($L_{\alpha }^M=L_{\alpha }$)

If $M$ is a transitive model of ZF, its internally computed $L_{\alpha }$ is the actual $L_{\alpha }$ for each ordinal $\alpha \in M$. At a successor stage use absoluteness of satisfaction for the same set structure, formula codes and parameters; at a limit stage take the union of the already identical earlier stages. Choice is not required.