Is model checking PSpace-hard *in formula size*?
You are certainly right that the level of rigor found in old papers making such claims can be a bit low at times when viewed from today's perspective.

The claim is correct anyway, even if it does not follow from Sistla/Clarke's proof. The reason is that LTL satisfiability checking is also PSPACE-complete. You can see satisfiability checking as a special case of model checking.

More formally, you want to prove the following: There exists a fixed model such that given an LTL formula, checking if the formula holds on the model is PSPACE-hard. Now the satisfiability checking problem does not restrict the number of atomic propositions, so a fixed model does not do the trick. However, S. Demri and P. Schnoebelen show in the paper "The complexity of propositional linear temporal logics in simple cases" (Inf. Comput., 174(1):84–103, 2002) that the satisfiability problem is hard even if we only have a single atomic proposition.