Traces and evidence

A formal model without grounding in reality is just theory. SpecLogician connects the formal specification to concrete evidence — test traces, production log traces, documentation references, and source code references. This connection works in both directions: evidence informs the model, and the model validates the evidence.

Artifact types

SpecLogician supports four kinds of artifacts:

Test traces

Structured records from test suites, each with concrete given/when/then values:

name:  "Order is rejected when qty exceeds max"
given: { pos = 0; rejected = 0 }
when:  { qty = 10001 }
then:  { pos = 0; rejected = 1 }

The given/when/then values are concrete IML expressions — specific values, not symbolic predicates. They represent one actual execution of the system.

Log traces

Records from production logs or message captures:

filename: "prod_2026-01-09_FIX.log"
contents: "8=FIX.4.4|35=D|11=abc123|38=10001|55=IBM|54=1|58=MaxQtyExceeded"
given:    { pos = 0; rejected = 0 }
when:     { qty = 10001 }
then:     { pos = 0; rejected = 1 }

Like test traces, the given/when/then values are concrete. The raw log contents are stored alongside for reference.

Documentation references

Pointers to requirements, specifications, or design documents:

text: "Order must be rejected if quantity exceeds max order size. max_qty=10000."
meta: "From requirements.md, section 3.2"

Source code references

Pointers to implementation code:

language:  python
file_path: risk/checks/order_limits.py
src_code:  "MAX_QTY = 10_000\n\ndef check_qty(order) -> bool:\n    return order.qty <= MAX_QTY"

Trace matching

The most important analysis for traces is scenario matching: does a concrete trace correspond to a formal scenario?

For each test trace or log trace with valid IML, ImandraX checks whether its concrete given/when/then values satisfy a scenario's symbolic predicates:

1. Given match — does the trace's concrete state satisfy the scenario's state predicates?
   • Trace: { pos = 0; rejected = 0 }, Scenario given: is_active (s.status = Active) → check if Active is the status when pos=0 and rejected=0
2. When match — does the trace's concrete action satisfy the scenario's action predicates?
   • Trace: { qty = 10001 }, Scenario when: qty_too_big (a.qty > 10000) → yes, 10001 > 10000
3. Then match — does the scenario's transition, applied to the trace's given state and action, produce the trace's then state?
   • Apply on_new_order to { pos = 0; rejected = 0 } with { qty = 10001 } → { pos = 0; rejected = 1 } → matches the trace's then

If all three match, the trace is linked to that scenario in the artifact map. A trace can match multiple scenarios (if scenarios overlap), and a scenario can be matched by multiple traces.

What unmatched traces mean

A trace that matches no scenario indicates one of:

• Missing scenario — the trace exercises a behavior that isn't formalized. You need to add a scenario that covers this case.
• Incorrect predicates — the scenario exists but its predicates don't match the trace's values. Adjust the predicates.
• Model gap — the domain base doesn't capture the dimensions the trace exercises. Extend the base types.

Unmatched traces are one of the primary drivers of model refinement. They tell you: "this real behavior happened, and your model doesn't account for it."

Artifact linking

Beyond automatic trace matching, you can manually link any artifact to any model component (predicate, transition, or scenario). This creates a traceability map:

• A documentation reference linked to qty_too_big → "this requirement grounds this predicate"
• A source code reference linked to on_new_order → "this code implements this transition"
• A test trace linked to reject_on_large_qty → "this test exercises this scenario"

The linked_artifacts_pct progress metric tracks what fraction of model components have at least one artifact link. The target is 100% — every predicate, transition, and scenario should be grounded in evidence.

Traces and reachability

Matched traces also feed into trace reachability. When a trace matches a sequence of scenarios, each consecutive pair is checked against the reachability graph. This connects the formal "what's possible" analysis to the concrete "what actually happened" evidence.

The evidence loop

Evidence and formal model evolve together:

1. Collect evidence — test traces, log traces, docs, source code
2. Build model — define base types, predicates, transitions
3. Add scenarios — formalize expected behaviors
4. Match traces — see which traces align with which scenarios
5. Find gaps — unmatched traces reveal missing scenarios; unlinked components lack grounding
6. Refine — add scenarios, adjust predicates, extend the base
7. Repeat

The model gets more precise with each iteration. Traces that were unmatched become matched. Components that were unlinked get evidence. The artifact map grows denser, and the gap between formal specification and real-world behavior narrows.