The difference between TP and formal verification

Stream: lean4

[Shaonan Wu]

Dear all,
I am curious about the distinction between theorem proving and formal verification when utilizing the Lean theorem prover. Specifically, I would like to know if Lean provides robust support for software formal verification similar to other provers like Isabelle.

In my opinion, theorem proving (TP) and formal verification (FV) may appear to be quite similar. Formal verification involves asserting properties of a function, which can be translated into theorems to be proven. I would appreciate it if you can explain the difference between these two tasks.

Thank you!

[Yaël Dillies]

The difference is not so fundamental. I would put it as such: Theorem proving involves few definitions and many theorems, software verification involves many definitions and relatively few theorems

[Kim Morrison]

Another dimension in which they are different is that mathematicians are surprisingly willing to do the grunt work themselves, but software verification needs/expects more automation. Lean is still missing some very significant pieces of automation, but we are hoping to make a lot of progress over the next year.

[Kim Morrison]

But as Yaël indicates, they are just the different names blind men are giving parts of an elephant.

[Shreyas Srinivas]

The computer science answer: formal theorem proving is one kind of formal verification. There are other kinds like model checking, smt solving etc. These categories are not mutually exclusive. There are theorem provers like TLA+ or Tamarin that are closer to the model checking side. Then there are theorem provers like lean in which you can embed model checking algorithms and prove their correctness more manually

[Kim Morrison]

And the converse to that is that we clearly want excellent model checkers, smt solvers, etc, in Lean. :-)