Technical Summary: Verified LLM-Driven Synthesis for Concept Design

Problem Statement

Modern software systems are increasingly assembled by composing reusable behavioral units (e.g., authentication, labeling, access control). While defining the behavior of individual units is often straightforward, specifying the coordination logic that ensures these units interact safely is difficult. The Concept Design methodology [Jac21] addresses this by organizing applications around "concepts" (self-contained, user-facing units of functionality) connected by "reactions" (synchronization rules).

However, Concept Design currently lacks a formal semantics for reactions. This absence makes it difficult to:

1. Precisely define what a design means.
2. Automatically verify that a design preserves safety invariants (e.g., "sensitive data must not remain in a dead-letter queue").
3. Synthesize safe coordination logic automatically.

Furthermore, even if a design satisfies a safety invariant, it may not match the user's intent. Many distinct reaction designs can satisfy the same invariant, including implausible ones (e.g., declassifying sensitive data to satisfy an invariant rather than moving the data). The paper identifies the need for a mechanism to steer synthesis toward the user's intended design without requiring the user to fully formalize their intent in complex logical constraints.

Methodology

The paper introduces foundry, a prototype tool that implements a Counterexample-Guided Inductive Synthesis (CEGIS) loop driven by Large Language Models (LLMs). The methodology consists of three core components:

1. Formal Semantics

The authors define an automata-based semantics for concepts and reactions:

• Concepts are modeled as initialized partial semiautomata (deterministic state machines with inputs but no outputs).
• Reactions are modeled as a partial monitor semiautomaton that observes the composed concept automaton. Reactions fire based on triggers (when), state conditions (where), and effects (then).
• Composition: The application is a synchronous composition of the concept automata and the reaction monitor.
• Verification Target: Safety is verified by checking that the application is "settled" (no pending obligations) exactly when the safety invariant holds. This is encoded in Alloy 6 and checked using bounded model checking.

2. LLM-Driven Synthesis Loop

The synthesis process operates as follows:

1. Proposal: An LLM proposes candidate reactions (or revises existing ones) to satisfy a given invariant.
2. Translation: A second agent translates the concept descriptions, reactions, and invariants (currently written in natural language) into Alloy 6.
3. Verification: The Alloy model checker verifies the candidate design against the invariant and any provided scenarios.
4. Feedback: If verification fails, the counterexample (a trace violating the invariant or scenario) is fed back to the LLM to refine the design.

3. Steering Mechanisms

To address the "underconstrained" nature of invariant-only synthesis, the paper proposes two steering mechanisms:

• Natural-Language Prompts: Providing textual descriptions of intended behavior alongside the invariant.
• Scenario-Guided Synthesis: Providing positive (allowed) and negative (forbidden) scenarios. Unlike prompts, scenarios have a formal semantics and can be automatically checked against candidate designs.
• Scenario Elicitation: An LLM-driven procedure where the model proposes short action prefixes that violate the invariant, and the user classifies them as desirable or undesirable. The model then proposes repairs (suffixes) for desirable prefixes. This shifts the user's task from authoring scenarios to classifying them.

Key Contributions

1. Formal Semantics: An automata-based semantics for Concept Design concepts and reactions, enabling bounded verification of invariants and scenarios.
2. Verified Synthesis Loop: A CEGIS-style, LLM-driven synthesis procedure for generating reaction designs, integrated with a scenario-guided mechanism to steer synthesis toward intended designs.
3. Scenario Elicitation: An LLM-driven technique to support early design exploration by having users classify proposed invariant-violating scenarios rather than authoring them from scratch.
4. Empirical Evaluation: A comprehensive evaluation on three applications (Dead-Letter Queue with sensitive data, Course Management System, One-Time Evidence Links) and twelve design variants using the GPT-5.5 LLM.

Results

The evaluation, conducted on a benchmark of 12 design variants, yielded the following findings:

• Invariant-Only Synthesis:

  • LLMs often reach a verified design quickly (often on the first attempt).
  • However, designs are rarely stable across runs.
  • Invariant-only synthesis frequently produces implausible designs (e.g., forbidding valid actions or declassifying data) because invariants alone underconstrain the design space.

• Scenario vs. Prompt Guidance:

  • Scenario-guided synthesis recovered intended designs more consistently than natural-language prompting (10/12 variants vs. 8/12 variants with initial inputs).
  • Scenarios are easier to revise mechanically (purely additive) compared to prompts, which can be brittle and ambiguous.
  • Overfitting: Minimal sets of scenarios can lead to overfitting, where the model fails to generalize (e.g., handling only specific cardinalities of messages). Adding scenarios with varied cardinalities mitigated this.

• Scenario Elicitation:

  • Eliciting 20 scenarios recovered the intended design in 9/12 variants, compared to 5/12 with 10 scenarios.
  • Non-determinism: The LLM's proposal of scenarios is non-deterministic; different runs elicit different sets of scenarios, leading to non-monotonic results (more scenarios do not always guarantee better coverage).
  • Missed Behaviors: If the elicitation process misses a critical scenario (e.g., a specific enrollment path), the synthesis may converge to a design that forbids that behavior, which was not the intent.

• Failure Modes:

  • The primary failure modes were missing critical scenarios (lack of coverage) and overfitting (failure to generalize).
  • Quality issues included redundant reactions and conditions, though these did not affect correctness relative to the invariant.

Significance and Claims

The paper claims that formal verification is essential when using LLMs for high-level design synthesis. While LLMs can often generate designs that satisfy simple invariants, they cannot be trusted to produce the intended design without additional steering.

The significance of the work lies in demonstrating that scenarios serve as effective, checkable steering artifacts. They bridge the gap between the formal safety requirements (invariants) and the user's informal intent. The paper argues that while invariants ensure safety, scenarios ensure plausibility and intent alignment.

The authors remain modest about the current state of the prototype:

• The translation from natural language to Alloy relies on an LLM, introducing a potential source of error (though manual inspection found no issues in the final verified designs).
• Verification is bounded; absence of counterexamples does not guarantee unbounded correctness.
• The evaluation is limited to one LLM configuration (GPT-5.5) and a specific set of benchmarks, though a cross-check with Claude Fable 5 showed similar success, suggesting the approach is not model-specific.
• Future work is required to replace LLM-based translation with a formal source language, scale verification to larger applications, and improve scenario elicitation to handle non-determinism and coverage gaps more robustly.