vstd_extra/temporal_logic/mod.rs
1// Copyright 2022 VMware, Inc.
2// SPDX-License-Identifier: MIT
3//! TLA temporal logic definitions and proof rules.
4//!
5//! Originally developed in the paper ["Anvil: Verifying Liveness of Cluster Management Controllers"](https://www.usenix.org/conference/osdi24/presentation/sun-xudong).
6//! Modified from the original version which can be found on [GitHub](https://github.com/anvil-verifier/anvil).
7pub mod defs;
8pub mod rules;
9
10pub use defs::*;
11pub use rules::*;