Related papers: Validating Traces of Distributed Programs Against …
TLA+ is a formal specification language used for designing, modeling, documenting, and verifying systems through model checking. Despite significant interest from the research community, knowledge about usage of the TLA+ ecosystem in…
Using an algorithm due to Safra for distributed termination detection as a running example, we present the main tools for verifying specifications written in TLA+. Examining their complementary strengths and weaknesses, we suggest a…
This paper presents our experience specifying and verifying the correctness of ZooKeeper, a complex and evolving distributed coordination system. We use TLA+ to model fine-grained behaviors of ZooKeeper and use the TLC model checker to…
In this paper I discuss how can lightweight formal methods be used to specify and verify software with complex configurations (for example, distributed protocols that work on specific network configurations). More specifically, I briefly…
TLA+ is a specification language based on standard set theory and temporal logic that has constructs for hierarchical proofs. We describe how to write TLA+ proofs and check them with TLAPS, the TLA+ Proof System. We use Peterson's mutual…
Developing and maintaining CLP programs requires visualization and explanation tools. However, existing tools are built in an ad hoc way. Therefore porting tools from one platform to another is very difficult. We have shown in previous work…
Offline runtime verification involves the static analysis of executions of a system against a specification. For distributed systems, it is generally not possible to characterize executions in the form of global traces, given the absence of…
Contracts specifying a procedure's behavior in terms of pre- and postconditions are essential for scalable software verification, but cannot express any constraints on the events occurring during execution of the procedure. This…
Alloy and TLA+ are two formal specification languages that are increasingly popular due to their simplicity and flexibility, as well as the effectiveness of their companion model checkers, the Alloy Analyzer and TLC, respectively.…
Programs with constraints are hard to debug. In this paper, we describe a general architecture to help develop new debugging tools for constraint programming. The possible tools are fed by a single general-purpose tracer. A tracer-driver is…
Large Language Models (LLMs) are unable to reliably reason about specific physical systems. Attempts to imbue LLMs with knowledge of the necessary physics concepts have shown great promise, but explainability and validation remain open…
Formal modelling is a powerful tool for developing complex systems. At MongoDB, we use TLA+ to model and verify multiple aspects of several systems. Ensuring conformance between a specification and its implementation can add value to any…
We discuss the workflows supported by the TLA+ Toolbox to write and verify specifications. We focus on features that are useful in industry because its users are primarily engineers. Two features are novel in the scope of formal IDEs:…
Formal theorem proving with TLA+ provides rigorous guarantees for system specifications, but constructing proofs requires substantial expertise and effort. While large language models have shown promise in automating proofs for tactic-based…
ZooKeeper is a coordination service, widely used as a backbone of various distributed systems. Though its reliability is of critical importance, testing is insufficient for an industrial-strength system of the size and complexity of…
TLAPS, the TLA+ proof system, is a platform for the development and mechanical verification of TLA+ proofs written in a declarative style requiring little background beyond elementary mathematics. The language supports hierarchical and…
Trace analysis can be a useful way to discover problems in a program under test. Rather than writing a special purpose trace analysis tool, this paper proposes that traces can usefully be analysed by checking them against a formal model…
What properties about the internals of a program explain the possible differences in its overall running time for different inputs? In this paper, we propose a formal framework for considering this question we dub trace-set discrimination.…
Fault-tolerant distributed algorithms are central for building reliable spatially distributed systems. Unfortunately, the lack of a canonical precise framework for fault-tolerant algorithms is an obstacle for both verification and…
Recent work has shown that Large Language Models (LLMs) are not only a suitable tool for code generation but also capable of generating annotation-based code specifications. Scaling these methodologies may allow us to deduce provable…