Maude executable specifications and analysis

Step 1: Define the semantics and claim

1. Record the model files/imports, initial states, state sort, environment/fairness assumptions, and required claim: data evaluation, sample execution, reachability, invariant, LTL, strategy-restricted behavior, or symbolic solutions.
2. Separate equations/axioms (state equality and normalization) from rules (transitions). Record equation termination/confluence/sort-decreasingness and rule coherence evidence or assumptions; Maude accepting a module proves none of these.
3. Read references/install-model-execute.md. Distinguish Core Maude from separately loaded Full Maude and extension tools; route Tamarin security-protocol work to tamarin-prover rather than translating its claims silently.
4. Review command files before loading. Files can contain arbitrary interpreter commands and IO; keep risky execution capabilities disabled for pure specifications. Bound potentially infinite computation and use a disposable workspace.

Gate: the model semantics, analysis mode, scope, assumptions, and executable trust boundary are explicit.

Step 2: Establish the executable environment