Here is the project where we keep annotations used by the PLAID group's static analyses, developed at Carnegie Mellon University.

Currently, annotation classes used by the Plural object protocol checker are available. Here is their documentation.

The FUSION (Framework Usage SpecificatIONs) project also uses these annotations. You can find documentation for how to use FUSION annotations on the FUSION wiki.