[tlaplus] Informal review of some TLA+ specs and TLAPS proofs (multi-agent control plane)

[Scott Cochran <scott.cochran@xxxxxxxxx>]

Hi,

I am looking for an informal review of some TLA+ specifications and TLAPS proofs: https://github.com/scottcochran/TOPAK, under spec/.

TOPAK is an architecture pattern for multi-agent systems that treats every agent as Byzantine and keeps the models out of the trusted computing base. The modules are small (a lease protocol, floor composition and routing, confinement, seating, observers, a coupling between a planner and an observer, break-glass, a workflow interpreter). About thirty are checked in TLC at small constants, with mutations that must fail, and 24 have TLAPS proof modules for their invariants. Liveness is checked by TLC and not proved. Seats.tla and Seats_proof.tla are a good two-minute first look.

All feedback is welcome.

Thanks,

Scott Cochran

-- 
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/CAAhV83fAY-LLUJjpN3-qBh%2B7XHxr%2B31WJOsJtsdRJ52qv7yD6w%40mail.gmail.com.