Mathematical descriptions of dynamical systems denote conjunctions of proof obligations—the advection–diffusion equation conserves mass and dissipates the L² energy—yet common task designs ask language models to summarize a system with a single structure label, a target wrong by construction for mixed systems. We recast the problem as autoformalization: translating natural language, equations, and stated assumptions into a typed formal specification whose atoms are machine-checkable matrix conditions on a linear state-space generator (A^⊤c=0, A^⊤M+MA=0, A^⊤M+MA⪯ 0, A^⊤J+JA=0). We release InvariantSpec: 12 dynamical systems × 5 linguistic variants × 3 modality conditions (180 inputs) with verifier-executable gold specifications, contrastive minimal pairs (boundary conditions, conserved vs. non-increasing, sentence order, linear vs. nonlinear generators), and two systems whose correct answer is not representable by a fixed linear generator. A symbolic verifier checks every predicted obligation and returns typed counterexample feedback; verified specifications are then compiled into constrained generators, including a projector-based parameterization conserving a linear quantity while dissipating a quadratic one. Across four frontier LLMs, single-label structure selection has exact specification match 0.00—a ceiling imposed by the answer space, not the models—while autoformalization with one round of verifier-guided refinement reaches up to 0.88 with soundness 0.98–1.00; the residual gap is dominated by unstated side conditions, not by obligation algebra. Downstream, one-step MSE does not predict long-rollout structural fidelity: spec-compiled generators satisfy every verified conservation or dissipation obligation over 1000-step rollouts (worst conservation defect 2.1×10^-10), while unconstrained models with equal or better MSE violate them by up to 10¹⁷.