Dear editors, this is a submission for the Special Issue on Neurosymbolic AI: First-Order Logic and Beyond. The paper presents a proof-guided neuro-symbolic framework for certifying, diagnosing, and repairing fairness in machine-learning systems. Causal structures learned from data support formal fairness derivations. Successful proofs yield machine-readable constraints for preserving certified properties, while diagnostic reports identify structural or statistical obstacles and guide causal model revisions or the construction of differentiable retraining losses. Kind regards Giuseppe Primiero