Looking for a few non-trivial TLAPS proof cases to improve a TLAPS agent skill

[younes-io]

Hi all,

I’m improving an agent skill that helps with TLAPS proof work, and I’m looking for a few non-trivial cases from real experience.

For context, one case I already have is:

• RaftElectionTLAPS.tla
• Prompt used: "$tlaps-workbench Model simplified Raft leader election (terms, votes). Prove leader uniqueness per term and monotonic term growth."

If you have ideas for "tricky/medium/advanced" TLAPS proofs, even just at idea level (no module/snippet required), I’d really appreciate them.

Useful info (any amount is fine):

• short description of the proof goal
• where/why it tends to get hard
• optional: module, theorem statement, or partial proof attempt

If you are open to follow-up discussion on your case, please say so (and how you prefer to continue). If not, no problem at all.

I’m not running a formal benchmark, just trying to improve the skill based on practical cases.

Thank you!

[muenchnerkindl]

Interesting work! If you are looking for further examples, here are some suggestions:

• EWD840,
• EWD998, note that the lemmas asserted but not proved about Fold could now be filled in based on FoldsTheorems and similar theorems in related Community modules,
• LamportMutex,
• Paxos.

Of course, the proofs for all these examples already exist, so probably the LLM would just draw them in. But perhaps you could vary the specs or theorem statements sufficiently so that they are not recognized directly.

[lemmy]

Indeed, cool work!

https://github.com/lemmy/BlockingQueue/blob/main/BlockingQueueSplit.tla and https://github.com/lemmy/BlockingQueue/blob/main/BlockingQueueFair.tla have a refinement proofs that may be worthwhile to recreate with AI. A more interesting experiment would to see if an AI can prove starvation freedom, for which no proof exists.

https://github.com/lemmy/BlockingQueue/blob/main/BlockingQueuePoisonPill.tla and https://github.com/lemmy/BlockingQueue/blob/main/BlockingQueuePoisonApple.tla lack safety and liveness proofs.

[lemmy]

Another idea: While the ultimate goal is to prove algorithms correct in terms of safety and liveness, the real challenge is often discovering the right inductive invariant.

A more approachable intermediate use case would be to use TLAPS to prove the equivalence of two TLA+ formulas. This could be especially helpful when refactoring a specification. Suppose a user has a complex formula F that they want to refactor into a new formula G. With TLC, the main option is to check F <=> G through model checking, which can be time-consuming and only provides bounded confidence.

Instead, TLAPS could be used to prove the equivalence directly:

THEOREM F <=> G
BY DEF F, G

This would provide a fast, unbounded proof that the refactoring preserves the meaning of the specification. This is something that I've done manually in the past.

[younes-io]

interesting use case, I'll look into this

[lemmy]

Partially related: https://github.com/YUH-Z/lmgpa by @YUH-Z, who will present their work at the upcoming TLA+ Community Event in April.