> What I'd like to see is something that does static analysis for reference-counted items.

This ought to be doable with GhostCell and similar efforts. https://plv.mpi-sws.org/rustbelt/ghostcell/ It doesn't cover the entire spectrum of "borrow safety proofs" but it can be used to address simple cases.