I agree that this API satisfies the property that one cannot cause UB using this API and only safe code. That is certainly a necessary condition for soundness, but it is not entirely clear that it is sufficient. (A precise definition of soundness is super hard -- a first version of that definition takes more than 100 pages in my PhD thesis -- so we usually just say that one must not be able to cause UB from safe code. But in this case I think that leads to the wrong conclusion.)
For example (not sure if this example was already brought up here; it is by Quy Nguyen), a client might call Pin::get_unchecked_mut and then re-assign the len field. This needs unsafe code, but all requirements of get_unchecked_mut are satisfied -- if we had a formal system for this, we could prove this code correct.
So clearly, if we combine the unsafe module that declares this pinned type, and the unsafe module that uses get_unchecked_mut, we can have UB. Which of the two modules is buggy? I think a good argument can be made that the get_unchecked_mut module is perfectly fine, since it diligently added safety comments to each unsafe operation and everything checks out. Therefore it must be the other module which is buggy -- the "soundness proof" of that module relied on an invariant involving the len field, but public fields cannot carry custom invariants.
Therefore I don't think pin projections are to blame here, this module was unsound to begin with.