Intro to TLA+ for the LLM Era: Prompt Your Way to Victory
30 points by zdw 3 days ago | 6 comments
leoqa 2 hours ago
Unfortunately the benefit of TLA+ is the act of modeling your system painstakingly. The actual checker helps confirm your hypothesis, etc. But skipping the modeling and outsourcing it is not ideal. I’ve always struggled reasoning about models my team mates wrote, and will often have to mentally go through the process of arriving at the same abstractions/invariants etc before I can understand it.
replyaerodexis 50 minutes ago
I did this myself a few weeks ago and the technique that helped me the most was to compare the TLA output against the race-conditions I could construct by hand. I worked iteratively and unit-tested the model by constructing a model that didn't have certain race protection mechanisms and validating that the model generated the expected race.
replyYou can also work backwards from the races it generates and ensure that they're real races.
"Running leading LLMs across the eleven systems shows that LLMs are great at producing correct TLA+ syntax but struggle to ensure conformance and appropriate invariants."
> It’s still your responsibility to understand your system and define what “correctness” means, and you need a high-level understanding of temporal logic.