No. Merged code can perform actions with effects on the world, even if a human being never saw it. Constructing a giant Lean formalization that nobody understands simply doesn't do anything.