Architecture of SpecLogician

SpecLogician is implemented in LangGraph as a state machine with transition functions modifying its internal state. Users (and their external AI agents) can interact with SpecLogician’s internal formalization state via MCP functions, which can be categorized as follows:

• Initialization and state management

  • create_thread: Start a new thread to create an empty graph state. This must be done before starting a new session.
  • init_state: Initialize the formalization state with a natural language spec. This must be done once per session, after create_thread.
  • get_nl_spec: Get the current version of the natural language spec.
  • set_source_spec: Manually update the natural language spec in the formalization state.
  • set_formal_spec: Manually update the FormalSpec source in the formalization state.

• Formalization

  • generate_formal_spec: Translate the current natural language spec into a formal specification using the FormalSpec DSL, taking into account previous attempts and validation results.
  • automatic_workflow: Run a fully automatic agentic workflow that translates the natural language spec into a formal specification, with automatic validation and retry logic (up to 3 attempts).
  • get_pprinted_formal_spec: Get the current formal spec in its human-readable, pretty-printed form.
  • get_ipl_spec: Compile the current formal spec to a formal state-machine representation in Imandra Protocol Language (IPL).

• User-initiated commands

  • set_user_instructions: Set user-provided instructions that provide additional context or technical details to guide the formalization process.
  • get_user_instructions: Get the list of user-provided instructions in the formalization state.
  • get_opaque_functions: Get a list of all opaque functions (functions with signatures but no implementations) in the current formal spec.
  • submit_fn_implementation: Manually set the implementation of opaque functions in the current formal spec using IPL statements.

• Validation

  • validate_formal_spec: Validate the current FormalSpec source and update the formalization state with validation results.
  • get_validation_result: Get the results of validating the current formal spec (requires validate_formal_spec to have been run).

• Synchronization

  • sync_nl_spec: Update the natural language spec to reflect edits made to the formal spec (useful when formal spec was modified directly).
  • sync_formal: Update the formal spec to reflect edits made to the natural language spec (behaves like generate_formal_spec but only if specs are out of sync).

Agentic workflow

Most of the functions exposed by SpecLogician MCP server as relatively fine-grained, and correspond 1-to-1 to a single state transition function in SpecLogician’s state machine implementation. This given flexibility to the user and their AI agents to have full control over the formalization process.

One important exception is the function automatic_workflow, which implements a fully automatic agentic workflow that combines several of the steps above to produce a valid formalization from the source natural language spec, with no external guidance required. Under the hood, the agentic workflow perform the following steps:

1. Attemp to generate a formal spec from the user’s natural language spec
2. Validate the generated formal spec
3. If the validation returns errors, and we are below 3 attempts, repeat from step 1. Otherwise, proceed.
4. Report the results to the user (including potential unresolved validation errors)