What surprised me in this experiment with Lean was that the AI-assisted formalization actually caught an error in my "vetted" TLA+ spec that had been sitting there for two years. It turns out my inductive invariant wasn't strong enough—something the TLA+ model checker didn't slap me for, but Lean’s kernel refused to ignore.
This was also a way to bridge a higher-level spec, written in Lean in a kind of TLA-like flavor, and the lower level implementation, also written in Lean but with a code-like flavor, and then proven that the implementation refines the spec.
Using Lean to bridge the gap between high-level temporal logic and low-level IO implementation, all written by AI but driven by human intent, feels like the first time the "coding singularity" might actually lead to better software rather than just more software