Symbolic execution limits in QWED

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 — see the Code engine reference 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:

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

Updated in v5.3.0. verify_code() and every other SymbolicVerifier public method now return a DiagnosticResult. The legacy dict shape (result["status"], result["is_verified"], result["functions_checked"]) is gone. See the Code engine migration guide 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

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.

boolean

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

string

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

string | None

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

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.

string

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

integer

Total functions found in the submitted code.

integer

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

integer

Functions that were proven by CrossHair without counterexamples.

integer

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

integer

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

integer

Number of concrete counterexamples produced by CrossHair.

integer

Number of per-function timeout issues reported.

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:

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)

verifier = SymbolicVerifier(timeout_seconds=5, max_iterations=10)

Balanced (default)

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

Thorough (slow, more coverage)

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

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:

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

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:

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:

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:

result = verifier.verify_code("x = 1 + 2\nprint(x)\n")

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

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.

Architecture

Concepts

Specifications

Integration Patterns

Contributing

Symbolic execution limits in QWED

The path explosion problem

When CrossHair works

When CrossHair fails

QWED’s bounded model checking solution

Fail-closed verification results

Result fields

Why untyped code fails closed

Configuration guide

Conservative (fast, less coverage)

Balanced (default)

Thorough (slow, more coverage)

Fallback strategy

Honest benchmarks

Best practices

Do use symbolic execution for

Don’t use symbolic execution for

API reference

Bounded model checking

Fail-closed result semantics

Result reason table

Typed function — no counterexample found

Untyped function — fails closed

Mixed typed and untyped — fails closed

Code with no functions — fails closed

Summary

​The path explosion problem

​When CrossHair works

​When CrossHair fails

​QWED’s bounded model checking solution

​Fail-closed verification results

​Result fields

​Why untyped code fails closed

​Configuration guide

​Conservative (fast, less coverage)

​Balanced (default)

​Thorough (slow, more coverage)

​Fallback strategy

​Honest benchmarks

​Best practices

​Do use symbolic execution for

​Don’t use symbolic execution for

​API reference

​Bounded model checking

​Fail-closed result semantics

​Result reason table

​Typed function — no counterexample found

​Untyped function — fails closed

​Mixed typed and untyped — fails closed

​Code with no functions — fails closed

​Summary

The path explosion problem

When CrossHair works

When CrossHair fails

QWED’s bounded model checking solution

Fail-closed verification results

Result fields

Why untyped code fails closed

Configuration guide

Conservative (fast, less coverage)

Balanced (default)

Thorough (slow, more coverage)

Fallback strategy

Honest benchmarks

Best practices

Do use symbolic execution for

Don’t use symbolic execution for

API reference

Bounded model checking

Fail-closed result semantics

Result reason table

Typed function — no counterexample found

Untyped function — fails closed

Mixed typed and untyped — fails closed

Code with no functions — fails closed

Summary