But the article doesn't deal with the possibility/impossibility of verification at all. It deals with the fact that (some?) specifications don't compose elegant

But the article doesn't deal with the possibility/impossibility of verification at all. It deals with the fact that (some?) specifications don't compose elegantly. That is, that a sufficient specification for System A and a sufficient specification for System B can't be trivially composed into a sufficient specification for a System C = System A + System B. That's not to say that System C can't be specified, but that it can't be specified without re-creating the specifications for System A and System B.