verus_temporal_logic

A Verus embedding of TLA+ temporal logic, ported from Anvil.

The crate provides:

• defs — Execution, TempPred, and the temporal connectives (always, eventually, leads_to, weak_fairness, valid, entails, tla_forall, tla_exists, stable, …).
• rules — verified TLA helper lemmas (modus ponens, weak-fairness, induction, monotonicity, ESR, etc.) for liveness and safety proofs.
• state_machine — Action, StateMachine, and NetworkStateMachine structs for defining state-transition systems with preconditions, transitions, and weak-fairness assumptions.

Execution Model

pub struct Execution<T> {
    pub nat_to_state: spec_fn(nat) -> T,
}

[dependencies]
vstd = { git = "https://github.com/verus-lang/verus.git" }
verus_temporal_logic = { git = "https://github.com/anvil-verifier/verus-tla" }

Build your local Verus binary following instructions in BUILD.md off the main branch of Verus.

See src/mutex_example.rs.

This crate uses cargo verus.

# Verify the library (defs + rules + state_machine)
cargo verus verify --lib

# Verify the mutex liveness example
cargo verus verify --bin mutex_example

MIT (inherited from the original anvil temporal_logic module).