formal-speclisted

# 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. ## Procedure ### Progress Checklist - [ ] Step 1: Extract properties from design - [ ] Step 2: Define state variables - [ ] Step 3: Write TLA+ specification - [ ] Step 4: Identify invariants - [ ] Step 5: Configure model checker - [ ] Step 6: Document assumptions and limitations ### Step 1: Extract Properties from Design Translate informal requirements into candidate formal properties: - **Safety properties**: "Bad thing never happens" — e.g., "No two processes hold the lock simultaneously" - **Liveness properties**: "Good thing eventually happens" — e.g., "Every request eventually gets a response" - **Security properties**: "U