Critical misalignments between ontological enterprise models and their implementations persist, causing behavioural inconsistencies and traceability gaps. To address this misalignment issue, the doctoral research presented in this paper develops a formal framework that refines ontological enterprise models into implementations with verifiable adherence to ontological constraints. The framework combines The framework combines (1) an ontological enterprise model, (2) its formally defined enterprise ontology, and (3) Correctness-by-Construction refinement. The framework, grounded in annotated first-order logic, is designed to ensure traceable correctness from an ontological enterprise model to an implementation. The anticipated results of the research are reduced implementation deficits and improved expertise amongst Enterprise Ontology practitioners through error-free refinements and enabling formal reasoning. Additionally, a formalised ontology is expected to strengthen model-driven development of Enterprise Ontology based information systems.