OLIVE: Output-Level Iterative Verification Engine

Large language models (LLMs) can effectively generate action plans from natural-language descriptions but provide no guarantees that their outputs satisfy domain-specific safety requirements. This limitation is particularly concerning in safety-critical domains such as emergency medicine, where protocol violations can jeopardize patient safety. We present OLIVE, a framework that combines LLM-generated plans with automated repair to automatically generate medical procedures with formally verified safety guarantees. OLIVE encodes established medical safety protocols as logical constraints in the Alloy specification language and verifies candidate plans against them. When verification identifies protocol violations, OLIVE incorporates the resulting counterexample directly into the generation loop to iteratively repair the candidate plan while preserving the LLM’s context-sensitive reasoning. We evaluate OLIVE on emergency medical scenarios derived from established clinical protocols and demonstrate that it automatically repairs protocol violations to produce plans that satisfy all specified safety requirements.