Comment by rubendev

I think at minimum you would need to understand which theorems you want to prove about your code, and how to express those in Lean. Otherwise you won’t be able to verify the output. It may have proven some statement that is machine checked to be correct, but it’s pointless if you don’t understand what that statement means and if it covers what you want to verify about your code.