Anomaly detection is crucial for identifying critical errors and suspicious behaviors.However, current methods struggle to explain why an input is anomalous in a rigorous manner.To address this explainability gap, we investigate counterfactual explanations supported by formal properties to ensure their quality.Given an anomalous input, our explanation is a "repair" highlighting what a non-anomalous analog should look like, removing the abnormality while preserving the normality and similarity to the input.We designed four properties that generalize across various domains, formulating a framework AR-Pro for explainable anomaly detection.Empirically, our framework produces semantically meaningful repairs that improve formal criteria by 96.14% on the VisA dataset for visual anomalies, and by 61.25% on the SWaT dataset for time-series anomalies.