Is There Any Way to Create and Validate Inductive Proofs?

[zicklag]

Is there any way to create and validate inductive proofs with Quint?

I'm still new to TLA+, but I've heard that there's a way to make inductive proofs in it. I've also written basic proofs in Coq and Lean, and I really like the idea of being able to prove safety invariants in my protocols.

Does Quint have anything along the lines of proofs instead of just model checking? Also, is there a way to know if a model checker has indeed checked every possible combination and essentially represents a proof of correctness?

[bugarela]

In model checking, we have the concept of inductive invariants, which has a similar basis as inductive proofs, but you don't need to construct an inductive proof yourself - the model checker verifies it for you. I like this section on the Apalache manual explaining inductive invariants.

So, for TLA+, you can use model checkers to verify inductive invariants. If you need inductive proofs, then you'd have to use TLAPM (which is a proof assistant just like Coq and Lean).

Quint should also support inductive invariants. Right now it is kinda flaky, but this is on our list of priorities for the next few months. The issue #1430 tracks work on it but also describes how one could do it currently.

---

Now for the last questions:

Does Quint have anything along the lines of proofs instead of just model checking?

Not really. You can transpile Quint to TLA+ and use proofs there, that's the closest you can get. Quint is not really targeted for people who can write proofs, so I don't see we adding that in the future. There are already pretty great proof languages, and you can't escape mathematics when doing proofs 😅.

Also, is there a way to know if a model checker has indeed checked every possible combination and essentially represents a proof of correctness?

Yes. If the model checker finishes executing (that is, quint verify finishes) and prints an [ok] result, in means it explored all possible executions of length up to --max-steps (10 by default) and could not break your property. You don't get guarantees for an arbitrary number of steps, unless you use an inductive invariant.

[zicklag]

Perfect, thanks! It took me a little looking around before I understood inductive invariants, but now I get it.

The idea is to validate that the inductive invariant holds:

• for every possible initialization state, and
• for every result you get applying next to every possible initialization state

If you can verify that, you only have to run the model checker one level deep and you can validate that the property hold for an infinite sequence of steps.

---

There are already pretty great proof languages, and you can't escape mathematics when doing proofs 😅.

Yeah, that's a great point. I suppose what I'm looking for is something like a bounded model checker and easy state machine syntax for Lean, but I think that's asking for a lot. 😁