This presentation, delivered by PhD student Ian Dardic of Carnegie Mellon University, introduces a novel, fully compositional framework for inductive invariant inference in TLA+. The work addresses the scalability limitations of formal verification tools like the TLC model checker, which struggle with infinite-state systems, and existing automated invariant inference tools that fail on complex specifications. The proposed "divide and conquer" methodology involves decomposing a TLA+ specification into smaller components, automatically inferring "assume-guarantee" contracts between them, and then inferring simpler, local inductive invariants for each component. The conjunction of these local invariants forms the global safety invariant. Key contributions include the karini tool, which automates contract inference using counterexample-guided inductive synthesis (CEGIS), and a new logic, Symbolic Fluent LTL (SFL), for expressing these contracts. The framework's effectiveness is demonstrated through three case studies, culminating in the semi-automatic verification of the complex static raft protocol, a task where global tools fail. This approach not only improves scalability but also yields more insightful artifacts, such as the automatic discovery of key protocol lemmas.
Automating TLA+ Proofs: A Divide and Conquer Approach
0:08:16 The Scalability Problem in Verification: The talk begins by highlighting the limitations of the TLC model checker, which cannot terminate on infinite-state systems or fully verify specifications with unbound constants. This necessitates more powerful proof methods.
0:10:20 Inductive Invariants as a Solution: Proofs by "inductive invariance" are introduced as a powerful technique for full verification. An inductive invariant is a formula that holds in the initial state, is preserved by every system step, and implies the desired safety property.
0:12:05 The Challenge of Complexity: Finding these invariants for real-world systems is extremely difficult. The presenter uses the static raft protocol as an example, which requires a highly complex 17-part invariant and over 1,500 lines of manual proof code.
0:13:40 A Compositional "Divide and Conquer" Framework: The core of the research is a new framework that breaks the problem down:
Decompose: The system specification is broken into smaller components.
Infer Contracts: "Assume-guarantee" contracts are automatically generated to define the interactions between components.
Infer Local Invariants: Simpler, local invariants are found for each component, a much easier task than finding the single global invariant.
0:15:45 Key Contributions & The karini Tool: The research produced a formal theory for this framework and a new tool, karini, which automates the contract inference step using a learning-based algorithm (CEGIS).
0:23:31 Symbolic Fluent LTL (SFL): A novel logic language, SFL, was developed to express the contracts. It uses "fluents" to track the history of actions (e.g., if a message was ever sent), which is key to defining component interactions.
0:31:08 How karini Works:karini learns the necessary assumptions by iteratively finding counterexamples and generating "blocking invariants" to rule them out, strengthening the assumption until it is sufficient to prove the property.
0:35:55 Case Study 1: Two-Phase Commit: For a smaller protocol, the compositional approach had a higher overhead (~3.5 minutes) compared to the global approach (~35 seconds).
0:37:43 Case Study 2: Database Server: For a larger specification, the compositional framework demonstrated its value, proving the system in 24 minutes versus 1 hour and 22 minutes for the global method.
0:38:24 Case Study 3: Static Raft: This is the flagship result. The global invariant inference tool failed completely on this complex, real-world protocol. The compositional approach enabled a semi-automatic proof in under 2 hours, reducing the local invariant complexity from 17 to a maximum of 9 conjuncts and the proof size from 1,500+ lines to under 200.
0:41:04 Uncovering Deeper Insights: A key takeaway is that the process yields valuable insights. karini automatically discovered and formulated the famous "one leader per term" lemma from the Raft protocol as part of its generated assumption, offloading a difficult part of the proof from the invariant inference step.
0:43:05 Future Work: The vision is to achieve full automation, extend the framework to handle liveness properties, and potentially build a new type of model checker that, instead of just failing, suggests the weakest assumption needed for a system to be correct.