Abstract
Formal verification is a subfield of computer science concerned with verifying the correctness of systems using mathematical techniques. It is easy to see from a cursory view that a pro-gram or protocol “does something,” but it is more difficult to see if it “does what you want it to do.” Formal verification allows developers to create a specification of a system that can be automatically verified as satisfying desired properties – formulating “what you want it to do” and proving it. One effective approach of formal verification is inductive invariant inference. An inductive invariant for a property P in a system S is a logical formula that: is true in ev-ery initial step (initiation); is closed under the transition relation (consecution); and implies the desired property P (safety). Intuitively, initiation and consecution ensure that is true in every state of the system, which combines with safety to ensure that P is also true in every state of the system. The general problem of inductive invariant inference is undecidable, so the compu-tational cost of inferring an inductive invariant rises exponentially as the input becomes more complex (Padon et al. 2016). Previous work by Dardik and Kang introduced a compositional inductive invariant inference approach. Instead of finding one inductive invariant for a mono-lithic system, the approach suggests decomposing the system into smaller components with as-sociated Assume-Guarantee contracts and then finding inductive invariants for each component. My contribution is a case study of using this approach on a TwoPhaseCommit TLA +protocol.
Recommended Citation
Nguyen, John
(2025)
"Compositional Verification in TLA+,"
The Crown: Syracuse Honors Research Journal: Vol. 2, Article 15.
Available at:
https://surface.syr.edu/thecrown/vol2/iss1/15
Poster - Compositional Verification in TLA+