Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

FASTRIC: Prompt Specification Language for Verifiable LLM Interactions

Wen-Long Jin

TL;DR

This paper tackles the lack of formal verification for multi-turn LLM interactions by introducing FASTRIC, a Prompt Specification Language that encodes explicit finite state machines within natural-language prompts. FASTRIC enables procedural conformance verification via execution traces, treating the LLM as an execution agent that follows designer-specified FSMs. It introduces a formality-based design parameter and a procedural conformance metric, and provides empirical evidence of model-specific Goldilocks zones where the specification level balances structure with interpreter capacity. The work offers a pathway to engineering verifiable, protocol-driven interactions across heterogeneous substrates, with potential impact on safe and reliable AI-enabled workflows.

Abstract

Large Language Models (LLMs) execute complex multi-turn interaction protocols but lack formal specifications to verify execution against designer intent. We introduce FASTRIC, a Prompt Specification Language that makes implicit Finite State Machines (FSMs) explicit in natural language prompts, enabling conformance verification through execution trace analysis. The LLM serves as intelligent execution agent: interpreting designer-encoded FSMs to execute specified behavioral roles. Unlike symbolic specification languages requiring parsers and compilers, FASTRIC leverages LLMs as unified infrastructure-simultaneously parser, interpreter, runtime environment, and development assistant. FASTRIC guides designers to articulate seven FSM elements (Final States, Agents, States, Triggers, Roles, Initial State, Constraints) structuring multi-turn interactions. Specification formality-ranging from implicit descriptions that frontier models infer to explicit step-by-step instructions for weaker models-serves as a design parameter. We introduce procedural conformance as verification metric measuring execution adherence to FSM specifications. Testing a 3-state kindergarten tutoring FSM across four formality levels and three model scales (14.7B, 685B, 1T+ parameters) reveals optimal specification formality is a function of model capacity. DeepSeek-V3.2 (685B) achieves perfect conformance (1.00) at L2-L4; ChatGPT-5 (~1T) peaks at L3 (0.90) before collapsing at L4 (0.39); Phi4 (14.7B) shows no stable optimum with high variance (SD=0.16-0.36). These findings reveal model-specific formality ranges-"Goldilocks zones"-where specifications provide sufficient structure without over-constraint, establishing Prompt Specification Engineering for creating verifiable interaction protocols, transforming multi-turn interaction design from heuristic art to systematic engineering with measurable procedural guarantees.

FASTRIC: Prompt Specification Language for Verifiable LLM Interactions

TL;DR

This paper tackles the lack of formal verification for multi-turn LLM interactions by introducing FASTRIC, a Prompt Specification Language that encodes explicit finite state machines within natural-language prompts. FASTRIC enables procedural conformance verification via execution traces, treating the LLM as an execution agent that follows designer-specified FSMs. It introduces a formality-based design parameter and a procedural conformance metric, and provides empirical evidence of model-specific Goldilocks zones where the specification level balances structure with interpreter capacity. The work offers a pathway to engineering verifiable, protocol-driven interactions across heterogeneous substrates, with potential impact on safe and reliable AI-enabled workflows.

Abstract

Large Language Models (LLMs) execute complex multi-turn interaction protocols but lack formal specifications to verify execution against designer intent. We introduce FASTRIC, a Prompt Specification Language that makes implicit Finite State Machines (FSMs) explicit in natural language prompts, enabling conformance verification through execution trace analysis. The LLM serves as intelligent execution agent: interpreting designer-encoded FSMs to execute specified behavioral roles. Unlike symbolic specification languages requiring parsers and compilers, FASTRIC leverages LLMs as unified infrastructure-simultaneously parser, interpreter, runtime environment, and development assistant. FASTRIC guides designers to articulate seven FSM elements (Final States, Agents, States, Triggers, Roles, Initial State, Constraints) structuring multi-turn interactions. Specification formality-ranging from implicit descriptions that frontier models infer to explicit step-by-step instructions for weaker models-serves as a design parameter. We introduce procedural conformance as verification metric measuring execution adherence to FSM specifications. Testing a 3-state kindergarten tutoring FSM across four formality levels and three model scales (14.7B, 685B, 1T+ parameters) reveals optimal specification formality is a function of model capacity. DeepSeek-V3.2 (685B) achieves perfect conformance (1.00) at L2-L4; ChatGPT-5 (~1T) peaks at L3 (0.90) before collapsing at L4 (0.39); Phi4 (14.7B) shows no stable optimum with high variance (SD=0.16-0.36). These findings reveal model-specific formality ranges-"Goldilocks zones"-where specifications provide sufficient structure without over-constraint, establishing Prompt Specification Engineering for creating verifiable interaction protocols, transforming multi-turn interaction design from heuristic art to systematic engineering with measurable procedural guarantees.

Paper Structure

This paper contains 28 sections, 3 figures, 3 tables.

Table of Contents

  1. Introduction
  2. Large Language Models: The unprecedented ability and the lack of formal verification
  3. FASTRIC: A Prompt Specification Language to Bridge Power and Verifiability
  4. Our Contributions
  5. Theoretical Foundations
  6. Formal Specification Languages and the FSM Foundation
  7. Multi-Agent Protocol Engineering and Dialogue Systems
  8. Natural Language Programming and Instruction-Following
  9. Convergence: Why Natural Language Specification Became Possible
  10. The FASTRIC Specification Language
  11. Design Foundations
  12. The Seven Elements and FSM Mapping
  13. Formality Levels as Control Variable
  14. Empirical Validation
  15. Experimental Design
  16. ...and 13 more sections

Figures (3)

  • Figure 1: Kindergarten math tutor FSM structure. State 0 (Init): student chooses EASY$\to$State 1 or HARD$\to$State 2. States 1--2 execute symmetric loops: ask question, wait for answer, evaluate answer, prompt navigation (MORE loops current state, CHANGE switches states).
  • Figure 2: Mean procedural conformance by model and formality level
  • Figure 3: Box plots show median (black line), interquartile range (box), full range (whiskers), and mean (white diamond).