> ## Documentation Index
> Fetch the complete documentation index at: https://docs.qwedai.tech/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 runs CrossHair only inside a Docker sandbox and addresses its limits with bounded model checking, depth limits, and graceful fallbacks. Every result is a [`DiagnosticResult`](https://docs.qwedai.tech/advanced/diagnostics) — see the [Code engine reference](https://docs.qwedai.tech/engines/code.md) for the full field map.

## Docker sandbox requirement

> [!NOTE]
>
> v8.0.0

CrossHair analyzes a function by importing its module, which runs the module's top-level code. QWED therefore runs CrossHair only inside a hardened Docker container. There is no host fallback.

The container has no network, a read-only root filesystem, no host mounts, and all capabilities dropped. It runs as user 65534 with `no-new-privileges` and the standard sandbox memory, CPU, PID, and concurrency limits. The submitted code reaches the container through its environment and is written only to a private tmpfs, so QWED writes nothing on the host.

### Prerequisites

* Docker running and reachable from the QWED process
* The `docker` Python package, installed by `qwed[symbolic]`
* The CrossHair sandbox image, built locally

```bash theme={null}
pip install "qwed[symbolic]"

# From a qwed-verification checkout
docker build -t qwed-crosshair-sandbox:0.0.101 docker/crosshair-sandbox
```

QWED never pulls the image at runtime. To use a different tag, set `QWED_CROSSHAIR_IMAGE`:

```bash theme={null}
export QWED_CROSSHAIR_IMAGE=registry.internal/qwed-crosshair-sandbox:0.0.101
```

If any prerequisite is missing, `verify_code()` returns `BLOCKED` with `constraint_id = "symbolic_verifier.runtime_unavailable"`:

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

result = verifier.verify_code(code)

if (result.status is DiagnosticStatus.BLOCKED
        and result.developer_fields["constraint_id"] == "symbolic_verifier.runtime_unavailable"):
    print(result.agent_message)  # Docker, a sandbox slot, the image, or CrossHair is unavailable
```

Code larger than 120 KiB returns `BLOCKED` with `constraint_id = "symbolic_verifier.input_too_large"` before QWED starts a container.

### How QWED reads CrossHair's outcome

The analyzed code runs in the same process tree as CrossHair, so it can influence the exit code. QWED trusts an outcome only when the in-container runner confirms it:

* A clean run is only ever "no counterexample found" (`UNVERIFIABLE`), never a proof.
* An exit code of 1 is a counterexample only when CrossHair's own report line (`<file>:<line>: error: ...`) is present. An early `os._exit(1)` from the analyzed code is an engine error.
* A `SystemExit` raised by the analyzed code while it is imported is an engine error, not a clean run.

### Function addressing

QWED addresses each function by its module qualname: `target.func` for top-level functions and `target.Class.method` for methods. CrossHair can't load nested functions by name, so QWED reports functions defined inside other functions as unverifiable.

## 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

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

`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

**status** `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, code too large, sandbox runtime unavailable). Read `developer_fields["constraint_id"]` for the specific reason.

**is\_verified** `boolean`

Convenience alias for `status is DiagnosticStatus.VERIFIED`. Always `False` for this engine.

**agent\_message** `string`

Layer 1 agent-safe summary of the outcome. Safe to surface to models — no rule IDs, detection logic, or internals.

**proof\_ref** `string | None`

Layer 3 proof reference. Always `None` for the Code engine.

**developer\_fields.constraint\_id** `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 and printed its own report line.
* `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.runtime_unavailable` — the Docker sandbox could not run CrossHair (no Docker, no free sandbox slot, missing image, CrossHair missing from the image, or the `docker` package not installed).
* `symbolic_verifier.input_too_large` — the submitted code exceeds 120 KiB.
* `symbolic_verifier.verification_error` — verification did not complete cleanly.

**developer\_fields.verification\_mode** `string`

`"symbolic"` for standard runs, `"bounded_symbolic"` for `verify_bounded()` runs.

**developer\_fields.functions\_discovered** `integer`

Total functions found in the submitted code.

**developer\_fields.functions\_checked** `integer`

Functions that were actually run through symbolic execution. A skipped function does not count as checked.

**developer\_fields.functions\_verified** `integer`

Functions that were proven by CrossHair without counterexamples.

**developer\_fields.functions\_skipped** `integer`

Functions skipped because they cannot be analyzed (for example, no type annotations).

**developer\_fields.functions\_unverifiable** `integer`

Functions that could not be proven, including skipped functions and functions whose verification raised an error.

**developer\_fields.counterexamples\_found** `integer`

Number of concrete counterexamples produced by CrossHair.

**developer\_fields.timeouts\_found** `integer`

Number of per-function timeout issues reported.

**developer\_fields.issues** `array`

Per-function issue records with `type` (`unverifiable`, `counterexample`, `timeout`, or `error`), `function` name, and `description`.

### 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 (`runtime_unavailable`, `input_too_large`, `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 reported at least one counterexample with its own report line. |
| `symbolic_verifier.timeout` | At least one function timed out. |
| `symbolic_verifier.incomplete_coverage` | At least one function was skipped, nested, 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.runtime_unavailable` | `BLOCKED`. Docker, a free sandbox slot, the sandbox image, CrossHair in the image, or the `docker` package is missing. |
| `symbolic_verifier.input_too_large` | `BLOCKED`. The submitted code exceeds 120 KiB. |

### 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."

## 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.


## Related topics

- [QWED Protocol: deterministic verification for LLMs](https://docs.qwedai.tech/whitepaper.md)
- [QWED deployment guide](https://docs.qwedai.tech/advanced/deployment.md)
- [Changelog](https://docs.qwedai.tech/changelog.md)
- [QWED MCP troubleshooting](https://docs.qwedai.tech/mcp/troubleshooting.md)
- [QWED protocol specification](https://docs.qwedai.tech/specs/qwed-spec.md)


This documentation is built and hosted on [Mintlify](https://mintlify.com), a developer documentation platform.