With the full support of ability checks via type constraints, the specification language would also be subject of ability checks. For instance, using exists<T>(addr) would require T to have the key ability.

However, this leads to breaking changes in existing code. Here is an example from the framework where T would required to be declared with the key ability:

  spec schema OnNewEpochAbortsIf<T> {
        ...
        aborts_if spec_fun_does_exist<T>(type_name) && !exists<T>(@aptos_framework);

This is probably ubiquitous also in user code.

For now, we have disabled ability checking in exp_builder (search for this bug number). We may want to revisit this and think about an upgrade path.