Verified LLM Synthesis Generates Safer Software Concept Designs

Concept Design structures software systems around user-facing units of functionality called concepts, composed via synchronization rules known as reactions. This paper by Alcino Cunha first establishes a formal semantics for concepts and reactions, enabling automatic verification of safety invariants—critical properties that must hold across all possible executions. Building on this foundation, the author presents a CEGIS-style (counterexample-guided inductive synthesis) LLM-driven procedure that generates reaction designs guaranteed to satisfy those invariants. Because many different designs can satisfy the same invariant, the work explores two methods to steer synthesis toward user intent: natural-language prompts and positive/negative example scenarios. A novel LLM-driven scenario elicitation technique is also proposed, where the user classifies proposed scenarios rather than authoring them from scratch, to support early design exploration.

The evaluation tested three applications and twelve design variants using a single LLM configuration. Invariant-only synthesis reached verified designs quickly but produced inconsistent and often implausible designs across runs, confirming that invariants alone underconstrain the design task. Scenario-guided synthesis recovered intended designs more consistently than natural-language prompting, though minimal scenarios risked overfitting. LLM-driven scenario elicitation recovered intended designs in most variants when enough scenarios were elicited, but missed behaviors and non-determinism prevented reliable coverage in all cases. These results highlight the inherent tension between formal correctness guarantees and capturing nuanced user preferences. The work suggests that combining formal verification with scenario-based guidance is a promising path forward for LLM-driven software design tools, but current techniques still struggle with completeness and behavioral coverage.