The way I understand it, the two implementations can only differ in the result if the lean translation was done incorrectly; that's the point, you don't want to use those to prove invariants in the next step.

For the next step, I have the same question. It's the crux of the approach and the article is surprisingly light on detail:

> The hardest part wasn't getting AI agents to write proofs. It was getting proofs that actually mean something

So it was done by AI but they don't make entirely clear how the interesting proof statements were chosen.