| Could you elaborate on what you mean by referring to TLA as a way to outline a proof? TLA stands for Temporal Logic of Actions, so it is a logic rather than a proof system – although the TLA paper [1] includes proof rules that can be (mainly) used in paper-and-pencil proofs. Like Coq and Lean, TLAPS is a mechanical proof assistant that allows you to write a detailed proof and have it checked by the system. These tools indeed require substantial effort from the user, but unlike model checkers such as TLC they can (in principle) verify correctness properties for arbitrary specifications, not only finite-state systems. Stephan
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 view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7D444807-747B-40F6-9AD9-EB3A203EADA3%40gmail.com. |