> ## Documentation Index
> Fetch the complete documentation index at: https://qwed-ai-mintlify-cfa51465.mintlify.site/llms.txt
> Use this file to discover all available pages before exploring further.

# Symbolic execution limits in QWED

> CrossHair symbolic execution limits in QWED — path explosion, deep loops, recursion, bounded model checking, and DiagnosticResult fail-closed semantics.

> **TL;DR:** CrossHair symbolic execution has real-world limitations. QWED addresses these with bounded model checking, depth limits, and graceful fallbacks. Every result is a [`DiagnosticResult`](/advanced/diagnostics) — see the [Code engine reference](/engines/code) for the full field map.

## The path explosion problem

Symbolic execution explores all possible execution paths. This works great for small code, but real-world code has:

| Challenge                | Example                | Impact                  |
| ------------------------ | ---------------------- | ----------------------- |
| **Deep loops**           | `for i in range(1000)` | 1000+ paths to explore  |
| **Recursion**            | `fibonacci(n)`         | Exponential path growth |
| **Complex conditionals** | Nested if/else chains  | 2^n paths               |
| **Data structures**      | Dict/list operations   | Unbounded state space   |

## When CrossHair works

| Code Type               | Works Well? | Example                            |
| ----------------------- | ----------- | ---------------------------------- |
| Pure functions          | ✅ Yes       | `def add(a, b): return a + b`      |
| Simple validation       | ✅ Yes       | `def is_positive(x): return x > 0` |
| Bounded loops           | ✅ Yes       | `for i in range(10)`               |
| LLM-generated utilities | ✅ Yes       | Most generated code is simple      |

## When CrossHair fails

| Code Type               | Works? | Why               |
| ----------------------- | ------ | ----------------- |
| Deep recursion (n > 50) | ❌ No   | Path explosion    |
| Unbounded loops         | ❌ No   | Infinite paths    |
| External I/O            | ❌ No   | Non-deterministic |
| Complex frameworks      | ❌ No   | Too much state    |

## QWED's bounded model checking solution

We implemented depth limits to prevent path explosion:

```python theme={null}
from qwed_new.core.symbolic_verifier import SymbolicVerifier
from qwed_new.core.diagnostics import DiagnosticStatus

verifier = SymbolicVerifier(
    timeout_seconds=30,   # Hard timeout per function
    max_iterations=100,   # Bounded model checking limit
)

result = verifier.verify_code(code)

if (result.status is DiagnosticStatus.UNVERIFIABLE
        and result.developer_fields["constraint_id"] == "symbolic_verifier.timeout"):
    # Fallback to a cheaper check
    print("Symbolic execution timed out, using static analysis")
```

## Fail-closed verification results

<Info>
  **Updated in v5.3.0.** `verify_code()` and every other `SymbolicVerifier` public method now return a [`DiagnosticResult`](/advanced/diagnostics). The legacy dict shape (`result["status"]`, `result["is_verified"]`, `result["functions_checked"]`) is gone. See the [Code engine migration guide](/engines/code#migrating-from-the-legacy-dict-api) for the field-by-field mapping.
</Info>

`verify_code()` is fail-closed: absence of proof is never reported as success. In fact, this engine **never emits `VERIFIED`** — CrossHair's search is timeout-bounded, not a completeness proof, so a clean run maps to `UNVERIFIABLE` with `constraint_id = "symbolic_verifier.no_counterexample_found"`. Treat symbolic-engine output as a bug hunter, not an authority.

### Result fields

<ResponseField name="status" type="DiagnosticStatus">
  `DiagnosticStatus.UNVERIFIABLE` for any incomplete or counterexample-producing run, or `DiagnosticStatus.BLOCKED` when verification could not be attempted at all (parse error, no functions, CrossHair missing). Read `developer_fields["constraint_id"]` for the specific reason.
</ResponseField>

<ResponseField name="is_verified" type="boolean">
  Convenience alias for `status is DiagnosticStatus.VERIFIED`. Always `False` for this engine.
</ResponseField>

<ResponseField name="agent_message" type="string">
  Layer 1 agent-safe summary of the outcome. Safe to surface to models — no rule IDs, detection logic, or internals.
</ResponseField>

<ResponseField name="proof_ref" type="string | None">
  Layer 3 proof reference. Always `None` for the Code engine.
</ResponseField>

<ResponseField name="developer_fields.constraint_id" type="string">
  Structured reason code. One of:

  * `symbolic_verifier.no_counterexample_found` — clean CrossHair run, still `UNVERIFIABLE` because completeness was not proven.
  * `symbolic_verifier.counterexample_found` — CrossHair disproved a check.
  * `symbolic_verifier.timeout` — verification did not converge within `timeout_seconds`.
  * `symbolic_verifier.incomplete_coverage` — at least one function could not be checked.
  * `symbolic_verifier.no_typed_functions` — no functions carried the type hints CrossHair requires.
  * `symbolic_verifier.no_verifiable_functions` — the source contained no functions.
  * `symbolic_verifier.syntax_error` — the code could not be parsed.
  * `symbolic_verifier.crosshair_not_available` — the CrossHair engine is not installed.
  * `symbolic_verifier.verification_error` — verification did not complete cleanly.
</ResponseField>

<ResponseField name="developer_fields.verification_mode" type="string">
  `"symbolic"` for standard runs, `"bounded_symbolic"` for `verify_bounded()` runs.
</ResponseField>

<ResponseField name="developer_fields.functions_discovered" type="integer">
  Total functions found in the submitted code.
</ResponseField>

<ResponseField name="developer_fields.functions_checked" type="integer">
  Functions that were actually run through symbolic execution. A skipped function does not count as checked.
</ResponseField>

<ResponseField name="developer_fields.functions_verified" type="integer">
  Functions that were proven by CrossHair without counterexamples.
</ResponseField>

<ResponseField name="developer_fields.functions_skipped" type="integer">
  Functions skipped because they cannot be analyzed (for example, no type annotations).
</ResponseField>

<ResponseField name="developer_fields.functions_unverifiable" type="integer">
  Functions that could not be proven, including skipped functions and functions whose verification raised an error.
</ResponseField>

<ResponseField name="developer_fields.counterexamples_found" type="integer">
  Number of concrete counterexamples produced by CrossHair.
</ResponseField>

<ResponseField name="developer_fields.timeouts_found" type="integer">
  Number of per-function timeout issues reported.
</ResponseField>

<ResponseField name="developer_fields.issues" type="array">
  Per-function issue records with `type` (`unverifiable`, `counterexample`, `timeout`, or `error`), `function` name, and `description`.
</ResponseField>

### Why untyped code fails closed

CrossHair requires type annotations to perform symbolic execution. Functions without type hints are reported as `skipped` and `unverifiable`, and the overall result fails closed:

```python theme={null}
result = verifier.verify_code("""
def add(a, b):
    return a + b
""")

assert result.is_verified is False
assert result.developer_fields["constraint_id"] == "symbolic_verifier.no_typed_functions"
assert result.developer_fields["functions_discovered"] == 1
assert result.developer_fields["functions_checked"] == 0
assert result.developer_fields["functions_skipped"] == 1
assert result.developer_fields["functions_unverifiable"] == 1
```

Mixed code that contains both typed and untyped functions also fails closed — a single skipped function is enough to keep `is_verified = False` and produce `constraint_id = "symbolic_verifier.incomplete_coverage"`. Code that contains no functions at all returns `BLOCKED` with `constraint_id = "symbolic_verifier.no_verifiable_functions"`.

Pre-verification exits (`crosshair_not_available`, `syntax_error`) return the same fail-closed shape — `is_verified` is `False` and function counters are absent from `developer_fields` — so callers can rely on `constraint_id` and `agent_message` regardless of how verification ended.

## Configuration guide

### Conservative (fast, less coverage)

```python theme={null}
verifier = SymbolicVerifier(timeout_seconds=5, max_iterations=10)
```

### Balanced (default)

```python theme={null}
verifier = SymbolicVerifier(timeout_seconds=30, max_iterations=100)
```

### Thorough (slow, more coverage)

```python theme={null}
verifier = SymbolicVerifier(timeout_seconds=300, max_iterations=1000)
```

## Fallback strategy

When symbolic execution fails, QWED falls back to:

```
1. Symbolic Execution (CrossHair)
   ↓ timeout/failure
2. Static Analysis (AST)
   ↓ insufficient
3. Type Checking (mypy patterns)
   ↓ still need more
4. Manual Review Flag
```

## Honest benchmarks

We tested CrossHair on different code types:

| Code Type       | Lines | Loops | Result         | Time |
| --------------- | ----- | ----- | -------------- | ---- |
| Simple math     | 5     | 0     | ✅ Verified     | 0.2s |
| String utils    | 15    | 1     | ✅ Verified     | 1.2s |
| Data validation | 30    | 3     | ✅ Verified     | 5.8s |
| Complex parser  | 100   | 10    | ⏱️ Timeout     | 30s  |
| Framework code  | 500+  | Many  | ❌ Not suitable | -    |

## Best practices

### Do use symbolic execution for

* ✅ LLM-generated utility functions
* ✅ Mathematical calculations
* ✅ Validation logic
* ✅ Simple transformations
* ✅ Code with clear contracts

### Don't use symbolic execution for

* ❌ Entire applications
* ❌ Code with external dependencies
* ❌ Deep recursion algorithms
* ❌ Real-time systems
* ❌ Code with I/O operations

## API reference

```python theme={null}
from qwed_new.core.symbolic_verifier import SymbolicVerifier

verifier = SymbolicVerifier(
    timeout_seconds=30,
    max_iterations=100,
)

# Estimate path budget before spending real time on verification.
budget = verifier.get_verification_budget(code, max_paths=1000)
if not budget.developer_fields["feasible"]:
    print("Code too complex for symbolic execution")

# Run symbolic verification.
result = verifier.verify_code(code)
```

### Bounded model checking

`verify_bounded()` applies loop and recursion bounds to the code before verification, then delegates to `verify_code()`. Every result sets `developer_fields["verification_mode"] = "bounded_symbolic"` and includes the applied bounds and the underlying complexity analysis. If the bounds transform itself fails (for example, the AST cannot be unparsed after transformation), the method returns `BLOCKED` with `constraint_id = "symbolic_verifier.bounds_transform_error"` instead of silently falling back to the original code:

```python theme={null}
result = verifier.verify_bounded(code, loop_bound=50, recursion_depth=20)

if result.developer_fields.get("constraint_id") == "symbolic_verifier.bounds_transform_error":
    print(result.agent_message)                      # Describes why the transform failed
    print(result.developer_fields["transform_error"]) # The underlying error message
```

## Fail-closed result semantics

`SymbolicVerifier.verify_code()` treats absence of proof as failure. The engine never emits `VERIFIED` — a clean CrossHair run is `UNVERIFIABLE` with `constraint_id = "symbolic_verifier.no_counterexample_found"`. Code that contains no functions, contains untyped functions, or mixes typed and untyped functions cannot ever appear as verified.

### Result reason table

| `developer_fields["constraint_id"]`         | When it applies                                                                              |
| ------------------------------------------- | -------------------------------------------------------------------------------------------- |
| `symbolic_verifier.no_counterexample_found` | Every checked function ran cleanly. Still `UNVERIFIABLE` because completeness is not proven. |
| `symbolic_verifier.counterexample_found`    | CrossHair returned at least one counterexample.                                              |
| `symbolic_verifier.timeout`                 | At least one function timed out.                                                             |
| `symbolic_verifier.incomplete_coverage`     | At least one function was skipped or errored.                                                |
| `symbolic_verifier.no_typed_functions`      | Every discovered function was skipped (for example, all untyped).                            |
| `symbolic_verifier.no_verifiable_functions` | The source contained no functions.                                                           |
| `symbolic_verifier.syntax_error`            | The submitted code could not be parsed.                                                      |
| `symbolic_verifier.crosshair_not_available` | The CrossHair engine is not installed.                                                       |

### Typed function — no counterexample found

```python theme={null}
from qwed_new.core.symbolic_verifier import SymbolicVerifier
from qwed_new.core.diagnostics import DiagnosticStatus

verifier = SymbolicVerifier(timeout_seconds=5)

result = verifier.verify_code("""
def add(x: int, y: int) -> int:
    return x + y
""")

result.status                                     # DiagnosticStatus.UNVERIFIABLE
result.developer_fields["constraint_id"]          # "symbolic_verifier.no_counterexample_found"
result.developer_fields["functions_checked"]      # 1
result.developer_fields["functions_verified"]     # 1
result.developer_fields["functions_unverifiable"] # 0
```

### Untyped function — fails closed

CrossHair requires type hints. Untyped functions are reported as skipped and unverifiable rather than silently passing:

```python theme={null}
result = verifier.verify_code("""
def add(a, b):
    return a + b
""")

result.is_verified                                 # False
result.developer_fields["constraint_id"]           # "symbolic_verifier.no_typed_functions"
result.developer_fields["functions_discovered"]    # 1
result.developer_fields["functions_checked"]       # 0
result.developer_fields["functions_skipped"]       # 1
result.developer_fields["functions_unverifiable"]  # 1
result.developer_fields["issues"][0]["type"]       # "unverifiable"
```

### Mixed typed and untyped — fails closed

Even if some functions verify, a single skipped function prevents an overall pass:

```python theme={null}
result = verifier.verify_code("""
def typed_add(a: int, b: int) -> int:
    return a + b

def untyped_add(a, b):
    return a + b
""")

result.is_verified                              # False
result.developer_fields["constraint_id"]        # "symbolic_verifier.incomplete_coverage"
result.developer_fields["functions_discovered"] # 2
result.developer_fields["functions_checked"]    # 1
result.developer_fields["functions_verified"]   # 1
result.developer_fields["functions_skipped"]    # 1
```

### Code with no functions — fails closed

Source that contains only top-level statements has nothing to prove and is reported as `BLOCKED`:

```python theme={null}
result = verifier.verify_code("x = 1 + 2\nprint(x)\n")

result.status                              # DiagnosticStatus.BLOCKED
result.developer_fields["constraint_id"]   # "symbolic_verifier.no_verifiable_functions"
```

<Warning>
  Do not gate downstream behavior on `is_verified` alone — for the Code engine it is always `False`. Downstream authority checks must inspect `result.proof_ref`, which this engine intentionally leaves as `None`. Use `developer_fields["constraint_id"]` for the specific reason and `developer_fields["functions_checked"]` to distinguish "no counterexample found" from "no symbolic proof was performed."
</Warning>

## Summary

| Question                                  | Answer                                                               |
| ----------------------------------------- | -------------------------------------------------------------------- |
| Does symbolic execution work on all code? | **No.** Limited by path explosion.                                   |
| How does QWED handle this?                | **Bounded model checking + fallbacks.**                              |
| What's the typical code size limit?       | **\~50-100 lines of simple code.**                                   |
| When should I use it?                     | **LLM-generated utilities and validation.**                          |
| Does this engine ever emit `VERIFIED`?    | **No.** CrossHair is timeout-bounded; a clean run is `UNVERIFIABLE`. |

***

*"My guess would be that technique falls apart at depths required in real world coding environments."*

— Reddit criticism. **We agree.** That's why we have bounds and fallbacks.