Sorry for burying this message.
I don't know that we'd talked about providing multiple names. My guess is that it ultimately won't be worth it: Some users will see a deprecated "Nonnull" annotation and assume (without reading the docs) that we don't have an annotation for that purpose at all; others will pick the wrong autocompletion by accident.
We do have work in front of us to simplify migration from one set of annotations to another. We put together some
similar migration tooling for the specific purpose of adapting the Checker Framework's annotated JDK to our requirements, and we have some other tooling inside Google for other migrations that we've performed. None of that is "ready," but it makes me confident that we can someday provide an experience in which users type `java jspecify-migration.jar` and then receive a set of changes that includes renames, import changes, and changes to annotation position if they're migrating from declaration annotations. If I'm right, then the naming will be one of the smaller obstacles to migration.