# Invariant Safety for Distributed Applications

## TL;DR

This paper introduces a modular and automated proof methodology for verifying safety invariants in highly-available distributed applications, enabling reasoning about individual operations and the application as a whole.

## Contribution

It presents a novel, automated, and modular proof technique that simplifies safety verification of distributed systems with replicated state.

## Key findings

- The methodology is automated and practical.
- It allows reasoning about distributed applications as if they were sequential.
- The approach is demonstrated on a representative example.

## Abstract

We study a proof methodology for verifying the safety of data invariants of highly-available distributed applications that replicate state. The proof is (1) modular: one can reason about each individual operation separately, and (2) sequential: one can reason about a distributed application as if it were sequential. We automate the methodology and illustrate the use of the tool with a representative example.