From the article, it is not clear how exactly verification using Lean uncovered those bugs.
It more looks like he started making assumptions about external dependencies, and start adding tests for testing those dependencies, and that's where bugs popped up.
It more looks like he started making assumptions about external dependencies, and start adding tests for testing those dependencies, and that's where bugs popped up.