Formal Specifications¶

This directory contains formal specification documents for the Fortress Rollback library.

Documents¶

Document	Description
formal-spec.md	Core formal specifications using TLA+ notation
api-contracts.md	API preconditions, postconditions, and invariants
determinism-model.md	Determinism requirements and verification
spec-divergences.md	Documented differences between spec and implementation