Core workflow

SpecLogician maintains mathematical context through a closed-loop cycle:

propose → formalize → verify → refine

The loop

1. RECON        Read code, collect artifacts (docs, source, tests, logs)
2. MODEL        Define domain base + predicates + transitions
3. SCENARIOS    Encode intended behaviors as given/when/then
                Mark desired outcomes --goal and failure modes --bad
4. EVIDENCE     Add test traces and log traces
5. INSPECT      View state, check diffs for improvements or regressions
6. DIAGNOSE     Check safety (reach safety), liveness (reach liveness),
                reachability, complement regions, inconsistencies
7. REFINE       Fix issues: safety violations, liveness violations,
                complement gaps, missing components
8. REPEAT       Go to step 5 until SAFE + LIVE + complement minimal

Who contributes what

Agent	Contribution
CodeLogician / ImandraX	Translate source code into formal models, provide symbolic analysis
LLM-powered CLIs	Propose scenarios, predicates, transitions as structured deltas
Software mapping tools	Provide high-level program structure and navigation context
Tests, logs, docs	Grounding evidence linked to formal components

Each agent contributes partial, local insight. SpecLogician integrates them into a single mathematical context and validates globally.

Why it closes the loop

The reasoning engine analyzes the entire accumulated model after every change. Local suggestions become globally validated — continuously.

Progress is measurable through diffs:

Metric	What it tells you
`scenarios_valid_pct`	Are all scenarios internally consistent?
`reachability_pct`	Can all scenarios be reached?
`components_valid_pct`	Does all IML compile?
`linked_artifacts_pct`	Is every component grounded in evidence?
`complement_regions`	How much behavior is unexplained?

Keeping context alive

As the system evolves, so does the mathematical context:

New code → update transitions and predicates
New tests → add test traces, check scenario matching
New requirements → add doc artifacts, create new scenarios
Bug discovered → the complement may already show the uncovered region

The model is never "done" — it's a living reference that stays aligned with the project.