One wrench to throw into this is that there are a lot of bugs around Lean and they have been incidentally exploited in the past. Hence, we still need a level of human verification today.