Thanks for the feedback! I should have explained the process more clearly. I first formalized security properties in Lean 4 (automatically extracted from Rust code) and attempted to prove them. All the bugs mentioned in the article were discovered by investigating failed proof attempts, and I then confirmed them with concrete tests against the original projects. So the Lean proof attempts came first, not the tests. I'll clarify this in the article!