Martin Kleppmann

I would suggest starting with model checking.

So something like TLA Plus or FISB are great.

much friendlier to getting started with compared to proof assistants like Isabel, Rock and Lean.

These proof assistants just require a whole lot of additional knowledge and the resources for learning about writing these formal proofs are, to be honest, not particularly good.

I haven't really found really great books on it as well.

The way I learned it was by working with some colleagues in my lab who had learned it through years of prior experience.

And I just sat down with them and paired with them at a desk where I described the thing I was trying to prove and they showed me how to prove it step by step, how to break it down.

Yes, I do hope so.

So the reason I think that I believe that this formal verification could become more important in the future is kind of several aspects to it.

One is that the LLMs are getting increasingly good at writing these proofs.

And if we don't have to write the proofs by hand as humans, it just becomes feasible to do them in situations where previously it would have not been economical.

But also, LLMs increase the need for these formal proofs because, you know, we're vibe coding a bunch of stuff.

If we have to manually review all of that code, then that will become the bottleneck.

So we can't really have humans reviewing all of the generated code either if we really want to get the benefits of AI.

So we need some automated way of checking whether the code is correct.

And writing lots of tests is a very good starting point.

but the thing that proof can do that tests can't is to consider absolutely every possible thing that could happen and that's really important in a security context for example where it just takes one little bug one to create a vulnerability that destroys the security of the whole system and so i feel for those domains where like really we want to ensure there's a complete absence of bugs

that's the kind of places where formal verification can really shine.

And I'm hoping that LLMs will actually make that a lot more accessible to people who would have previously not considered using formal verification because it was just too hard and too expensive.

Yeah, within academia, there are lots of different styles, really.