andriy_koval
17 hours ago
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.
syumei
16 hours ago
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!