---

In this talk, the speaker will present ongoing work of applying formal verification to two Open Radio Access Networks (O-RAN) scenarios. First scenario will be safeguarding resource allocation optimisation AI/ML-driven applications (xApps) generated by Large Language Models (LLMs) and computing optimal thresholds between energy efficiency and service availability using the PRISM model checker.