This package defines a language for replicated transactions.

Transactions written in this language can be verified to preserve application-specific state invariants and pre/post specifications, even when they depend on fine-grained coordination rules to uphold those specifications.