Re: [tlaplus] Tools enhancements in "Smart Casual Verification of the Confidential Consortium Framework"

Good list! I had only heard about 3 and 5.

For now unfortunately the answer for where you can learn more about them is "nowhere outside of reading PRs", although Markus does post some demo videos on the TLA+ youtube channel: https://www.youtube.com/@TLAplusFoundation/videos

I think the best way to document these features is to write a bunch of how-to docs on docs.tlapl.us. Using the schema of documentation being split into tutorials, how-to guides, explanation, and reference (from here), I think docs.tlapl.us is a great place to put how-to-guides and conceptual explanations. We are pretty well covered for TLA+ tutorials with Hillel's learntla.com and Leslie's various courses & books, and I think wikis probably aren't a good place for reference documentation, but how-to-guides and conceptual explanations seem like the perfect fit for the docs.tlapl.us wiki. Of course I'm not married to it and we could do something like readthedocs.io instead.

As for who should do the work of writing all the how-to guides, it seems like a good target for foundation funding. After I finish my current project of transitioning TLAPM to use SANY I might be up for it. I do enjoy technical writing. But it's a lot to write and I would be happy to share the load!

Andrew Helwer

On Mon, May 19, 2025 at 7:45 PM A. Jesse Jiryu Davis <jesse@xxxxxxxxxxxxxxx> wrote:

Hello, I'm reading "Smart Casual Verification of the Confidential Consortium Framework". Markus is a co-author. It's great! The authors succeeded where I had failed and they clearly describe how they did it.

The paper mentions new features in the TLA+ tools:
"we manually weighted failure actions to reduce the likelihood of them being chosen"
"we implemented depth-first search (DFS) in TLC"
"TLC had already been enhanced to support trace validation"
In the TLA+ debugger, "we implemented a new unsatisfied breakpoint that activates for each state in T that is found to be unreachable"
"T can be visualized as a graph that not only includes all unreachable states but also references the subformula responsible for the state being unreachable"
The paper summarizes this effort as "enhancing the TLC model checker to support trace validation, which involved implementing support for action composition, DFS, improved debugging support, and visualizing the state graph." So I think the enhancements are in both TLC and the VS Code TLA+ debugger.

Question: Am I right that the paper mentions 6 new features, and where can I learn more about them?

Thanks, I know I'm asking for a lot of info.

--
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 visit https://groups.google.com/d/msgid/tlaplus/2443fd1a-1c35-419a-95b8-72de361f28bdn%40googlegroups.com.