「非nullのint配列」をアノテーションで表すのは `＠NonNull int[]` ではない

正解は int ＠NonNull [] です。な、なんだってー！

本当です。Java言語仕様書にも記載がありますが、配列を修飾する場合は [] の手前にアノテーションを書く必要があります。JVM仕様書に記載の例のほうがわかりやすいかもしれません：

@Foo String[][]   // Annotates the class type String
String @Foo [][]  // Annotates the array type String[][]
String[] @Foo []  // Annotates the array type String[]

組み合わせて考えると、「要素も配列自体も非nullのString配列」は @NonNull String @NonNull [] になります。コレクションは @NonNull List<@NonNull String> みたいにわかりやすいんですけどね。JavaのRecordでは配列を使わないほうが良いという話の時にも思いましたが、Javaは配列周りに非直感的な挙動が多い気がします。

なお配列だけでなく内部クラスでも同様で、パラメータが非nullの内部クラスを要求することをアノテーションで表現する場合は @NonNull Outer.Inner param ではなく Outer. @NonNull Inner param と内部クラス名の手前にアノテーションを書く必要があります。これTwitterで11名にアンケートご協力いただいた限りでは、正答を答えられたのは1名だけという難問でした。

他にアノテーション周りで驚く機能としては、 this を修飾する方法も提供されています。receiver parameterと言います。Pythonのように第1引数にthisを書く形です：

class MyClass {
  void method(@Foo MyClass this, String param) {
    // ...
  }
}

いずれもJava8（2014年）からあった機能ですが、自分は今日まで知りませんでした。クラスファイルパーサを書くことが無ければ、このまま気づかなかったかもしれないです。Java、奥が深い。