I disagree - in safe code, the meaning of & and &mut are quite well-defined: & is multiple aliases may exist but mutation may not occur while borrowed, and &mut means that only one such reference may exist, and mutation can occur through it.
Unless the Nu levels are implemented, this is sufficient, and work on this can proceed.
Furthermore, even aside from that, a “safer ABI based on Rust” does not necessarily need to have exactly Rust’s definition of unsafe - it may, in fact, end up being prudent to ban the Nu levels entirely, or say that the aliasing/mutability guarantees of references from this ABI may never be violated, even within unsafe.
Either of those would suffice.