I am developing a formalization of Gödel's constructible universe in Lean 4.
Here you can find the github repository for the project.
It presently incorporates the construction of the L-hierarchy and the proof of the Axiom of Extensionality.
The construction of the L-hierarchy starts just from a wellorder R, and letting gamma be the ordertype of R, defines L_gamma in the codes determined by R. Thus, it does not rely on any general development of set theory; only wellorders (and recursion along the wellorder).