-
Notifications
You must be signed in to change notification settings - Fork 1
Overview
github-actions[bot] edited this page Mar 29, 2026
·
3 revisions
This directory contains formal specification documents for the Fortress Rollback library.
| 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 |
- TLA+ Specifications - Runnable TLA+ model checking specifications
- Z3 Verification Tests - Z3 SMT solver verification tests