Formal Spec

Purpose

Extract properties from a system design, define state variables, write TLA+ specifications, identify invariants, configure the TLC model checker, and document assumptions and limitations.

Scope Constraints

Reads system designs, protocol descriptions, and existing specifications. Produces TLA+ specification files as output. Does not execute model checkers or modify implementation code.

Inputs

• System design or protocol description to formalize
• Security properties that should hold (informally stated)
• Concurrency model (number of processes, shared state, communication mechanism)
• Scope constraints (bounded checking parameters)
• Existing informal specification or documentation

Input Sanitization

No user-provided values are used in commands or file paths. All inputs are treated as read-only analysis targets.