• Specification anti-patterns
• Too much syntactic sugar
• Overpopulated core hint database
• Module structure anti-patterns
• One-big-file approach
• Unscoped, global, top-level notations
• Proof structure anti-patterns
• Linear multi-goal proofs
• Over-nesting bullets
• No names
• Non-monotone automation