Integrations

SpecLogician is designed to be the formal backbone in an agentic toolchain.

CodeLogician / ImandraX

  • Translate source code into formal models and reasoning artifacts
  • Provide decomposition/verification results
  • Enable global analysis after every change

If codelogician is installed, use it as an IML companion: draft and validate IML snippets before feeding them into SpecLogician.

LLM-powered agentic CLIs

SpecLogician is built for agent consumption:

  • All commands support --json for structured, parseable output
  • Batch operations (ch batch --json) apply many changes with one analysis pass
  • --dry-run validates batches cheaply before committing
  • Structured error responses include stage, change_index, and error.message
  • Progress metrics (scenarios_valid_pct, reachability_pct, etc.) give agents clear optimization targets
  • speclogician prompt generates a comprehensive agent instruction guide

Recommended agent loop:

1. RECON       Read code, collect artifacts (doc-add, src-add)
2. MODEL       Define domain base + predicates + transitions (ch batch)
3. SCENARIOS   Encode behaviors as given/when/then (ch batch)
               Mark desired outcomes --goal and failure modes --bad
4. EVIDENCE    Add test/log traces
5. INSPECT     view state --compact && view diff --json
6. DIAGNOSE    reach properties && reach unreachable
7. REFINE      Fix safety violations (bad reachable), liveness violations
               (goal unreachable), complement gaps
8. REPEAT      Until SAFE + LIVE + progress metrics reach targets

Software mapping tools (e.g. CodeMaps)

  • Provide high-level program structure and navigation context
  • Help agents focus on relevant subsystems

SpecLogician integrates partial local insights into one evolving, validated formal state.

Previous← Reachability commands
NextExamples →