AI tells me that code using the verus! macro everywhere would double in build time but if only used ocassionally the verus! macro would only increase build time

AI tells me that code using the verus! macro everywhere would double in build time but if only used ocassionally the verus! macro would only increase build time by a few percent. The attribute annotation would basically be free, but there is a downside that loop invariants would be rejected by stable rustc.