interactive theorem provers such as Isabelle (underlying the SEL4 project) and model checkers are very different beasts. The former can be used to verify systems of arbitrary complexity, and in particular infinite-state systems, whereas model checking imposes restrictions that ensure that the verification problem is decidable. In particular, the TLA+ model checker TLC is restricted to verify finite-state instances. Most errors can be found over small instances (say, a 3-process version of your algorithm), but it is not always clear if the algorithm is correct in general when the model checker does not find an error for the instances that it can check.
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/57F9C4E3-CB44-4792-8828-AC7F0F27EFD9%40gmail.com.
For more options, visit https://groups.google.com/d/optout.