Verified LLM-Driven Synthesis for Concept Design

foundry is a small command-line tool for turning partial Concept Design app descriptions into complete app designs. It asks an LLM to propose reactions, translates the design to Alloy, checks the resulting model, and iterates when Alloy finds counterexamples. It can also verify completed designs and generate new scenarios for a user to classify. Foundry and its evaluation are described in Verified LLM-Driven Synthesis for Concept Design.

Requirements

• Python 3.9 or later. No third-party Python packages are required when using codex-cli.
• An Alloy command-line executable available as alloy, or passed with --alloy-exec
• Access to at least one supported model platform: codex-cli, claude-api, gpt-api, or deepseek-api

For direct API access, install the corresponding optional Python package:

pip install anthropic  # claude-api
pip install openai     # gpt-api or deepseek-api

Set ANTHROPIC_API_KEY, OPENAI_API_KEY, or DEEPSEEK_API_KEY as appropriate for the selected API platform.

Foundry can infer the platform from common model names, or you can pass --platform, --platform-reactions, --platform-alloy, or --platform-scenarios explicitly.

App Descriptions

A partial app usually contains the application name, types, concepts, and invariants:

application: NoDeadSensitiveMessages
types:
    a set Message
    a set Tag
    one special Tag named Sensitive
concepts:
    one DeadLetterQueue[Message] named Q
    one Label[Message,Tag] named L
invariants:
    there are no dead messages in Q labeled with Sensitive in L

Complete apps may also include scenario classifications and synchronizations:

scenarios:
    nok: Q.submit(m); L.affix(m,Sensitive); Q.fail(m)
    ok:  Q.submit(m); Q.fail(m); L.affix(m,Sensitive); Q.retry(m)
synchronizations:
    reaction retry_sensitive_dead_message
    when
        L.affix(m,Sensitive)
    where
        m is in dead in Q
    then
        Q.retry(m)
    reaction prevent_sensitive_failure
    when
        Q.fail(m)
    where
        Sensitive is a label of m in L
    then
        error

Concept definition files can be supplied with --concept-files. If omitted, Foundry tries to infer files such as DeadLetterQueue.md and Label.md from the app's concepts section.

Usage

Show the available commands:

python3 foundry.py --help

Synthesize reactions for a partial app and validate them with Alloy:

python3 foundry.py synthesize \
  --model-reactions gpt-5.5 \
  --model-alloy gpt-5.5 \
  examples/NoDeadSensitiveMessages1Scenarios.md

Interactively synthesize reactions from Alloy counterexamples:

python3 foundry.py interactive \
  --model-reactions gpt-5.5 \
  --model-alloy gpt-5.5 \
  --num-alternatives 3 \
  examples/NoDeadSensitiveMessages1Scenarios.md

Verify a complete app description:

python3 foundry.py verify \
  --model-alloy gpt-5.5 \
  examples/NoDeadSensitiveMessages1.md

Generate new scenarios and classify them interactively:

python3 foundry.py scenarios \
  --model-scenarios gpt-5.5 \
  examples/NoDeadSensitiveMessages.md

Commands

• synthesize: generates reactions, checks the design invariant, checks scenario expectations, and asks the model to repair the app when needed.
• interactive: starts with no reactions, shows each Alloy counterexample, asks the model for alternative fixes, and lets the user choose which reactions to keep.
• verify: translates a completed app to Alloy, checks the Design property, and checks generated scenario run commands.
• scenarios: proposes new scenarios one at a time, asks the user to mark each as ok, nok, skipped, or quit.

Generated app versions, Alloy modules, Alloy logs, and counterexample traces are written to tmp/ by default. Use --output-dir to choose another directory for commands that produce Alloy artifacts.

The synthesize, interactive, and scenarios commands save the resulting app to <appname>_<model>.md by default. Use --output-file to choose another file.

Alloy-backed commands use a default top-level Design check scope of 3. Pass --top-scope N or --default-scope N to override it.

Evaluation Artifacts

The paper evaluation uses one model configuration, gpt-5.5, with default sampling settings. The experiments were run on three benchmark applications and twelve intended design variants. The hand-written intended designs are the ApplicationN.md files in examples/; the generated designs are the corresponding *_gpt-5.5*.md files.

Benchmark

Application	Concepts	Intended variants
NoDeadSensitiveMessages	DeadLetterQueue, Label	1, 2, 3, 4
CourseManagementSystem	Rostering, Registration	1, 2, 3, 4
OneTimeEvidenceLinks	Vault, Permalink	1, 2, 3, 4

Verification Timing

RQ1 measures Alloy verification time for the hand-written intended designs while varying scope and bounded steps. The reproducibility script is scripts/benchmark_verification_times.py; by default it benchmarks the twelve intended variants above.

Invariant-Only Synthesis

RQ2 runs synthesis three times per application with only the safety invariant as guidance. Each link below is the final generated design for that run.

Application	Runs
NoDeadSensitiveMessages	1, 2, 3
CourseManagementSystem	1, 2, 3
OneTimeEvidenceLinks	1, 2, 3

Prompt- and Scenario-Guided Synthesis

RQ3 compares natural-language prompts with classified scenarios. Each variant has an intended design, an initial prompt input, and an initial scenario input. Some inputs were revised once after initial failures; revised runs are listed in the last two columns when present.

Variant	Intended	Prompt runs	Scenario runs	Revised prompt runs	Revised scenario runs
NoDeadSensitiveMessages 1	design	input; 1, 2, 3	input; 1, 2, 3
NoDeadSensitiveMessages 2	design	input; 1, 2, 3	input; 1, 2, 3
NoDeadSensitiveMessages 3	design	input; 1, 2, 3	input; 1, 2, 3
NoDeadSensitiveMessages 4	design	input; 1, 2, 3	input; 1, 2, 3		input; 1, 2, 3
CourseManagementSystem 1	design	input; 1, 2, 3	input; 1, 2, 3
CourseManagementSystem 2	design	input; 1, 2, 3	input; 1, 2, 3
CourseManagementSystem 3	design	input; 1, 2, 3	input; 1, 2, 3
CourseManagementSystem 4	design	input; 1, 2, 3	input; 1, 2, 3	input; 1, 2, 3	input; 1, 2, 3
OneTimeEvidenceLinks 1	design	input; 1, 2, 3	input; 1, 2, 3	input; 1, 2, 3
OneTimeEvidenceLinks 2	design	input; 1, 2, 3	input; 1, 2, 3	input; 1, 2, 3
OneTimeEvidenceLinks 3	design	input; 1, 2, 3	input; 1, 2, 3
OneTimeEvidenceLinks 4	design	input; 1, 2, 3	input; 1, 2, 3	input; 1, 2, 3

Scenario Elicitation

RQ4 asks the model to elicit classified scenarios before synthesis. For each variant, the 10 scenarios and 20 scenarios links point to the elicited scenario batch, followed by the three synthesis runs generated from that batch.

Variant	10 scenarios	20 scenarios
NoDeadSensitiveMessages 1	batch; 1, 2, 3	batch; 1, 2, 3
NoDeadSensitiveMessages 2	batch; 1, 2, 3	batch; 1, 2, 3
NoDeadSensitiveMessages 3	batch; run 1 failed, 2, 3	batch; 1, 2, 3
NoDeadSensitiveMessages 4	batch; 1, 2, 3	batch; 1, 2, 3
CourseManagementSystem 1	batch; 1, 2, 3	batch; 1, 2, 3
CourseManagementSystem 2	batch; 1, 2, 3	batch; 1, 2, 3
CourseManagementSystem 3	batch; 1, 2, 3	batch; 1, 2, 3
CourseManagementSystem 4	batch; 1, 2, 3	batch; 1, 2, 3
OneTimeEvidenceLinks 1	batch; 1, 2, 3	batch; 1, 2, 3
OneTimeEvidenceLinks 2	batch; 1, 2, 3	batch; 1, 2, 3
OneTimeEvidenceLinks 3	batch; 1, 2, 3	batch; 1, 2, 3
OneTimeEvidenceLinks 4	batch; 1, 2, 3	batch; 1, 2, 3

The paper also discusses recurring failure modes in these scenario-guided runs: missing critical scenarios, overfitting to minimal scenarios, occasional model misbelief that scenarios are inconsistent, and redundant reactions or conditions in otherwise intended designs.

Acknowledgements

This work was financed by National Funds through the FCT - Fundação para a Ciência e a Tecnologia, I.P. under the PRR - Recovery and Resilience Plan, within the scope of the Science + Training measure, within grant FCT/Mobility/1355087736/2024-25.