Code engine

Updated in v5.3.0 (breaking). Every SymbolicVerifier public method now returns a DiagnosticResult instead of an ad-hoc dict. See the migration section for a field-by-field mapping. The Code Engine is the first fully DiagnosticResult-conformant engine and serves as the reference implementation for future engine migrations.

The Code Engine uses CrossHair, a symbolic execution tool for Python, to verify code properties without running it.

Capabilities

Feature	Description
Symbolic verification	CrossHair-driven property checking on typed functions
Contract verification	Precondition and postcondition assertions
Safety analysis	Division-by-zero and index-out-of-bounds hazards
Bounded model checking	Verify under explicit loop and recursion bounds
Complexity analysis	Loops, recursions, and path-budget estimates

Quick start

from qwed_new.core.symbolic_verifier import SymbolicVerifier

verifier = SymbolicVerifier()

code = """
def divide(a: int, b: int) -> float:
    return a / b
"""

result = verifier.verify_code(code)
print(result.status)               # DiagnosticStatus.UNVERIFIABLE
print(result.is_verified)          # False
print(result.agent_message)        # "Symbolic verification found a counterexample..."
print(result.developer_fields["constraint_id"])
# "symbolic_verifier.counterexample_found"

Every method on SymbolicVerifier returns a DiagnosticResult with the same three layers described in Verification Diagnostics: a Layer 1 agent_message, a Layer 2 developer_fields dict, and a Layer 3 proof_ref (always None for this engine — see Why VERIFIED is never emitted).

The `DiagnosticResult` contract

All six public methods — verify_code, verify_function_contract, verify_safety_properties, verify_bounded, analyze_complexity, get_verification_budget — return a DiagnosticResult.

Status values

`result.status`	Meaning
`DiagnosticStatus.VERIFIED`	Never emitted by this engine. See below.
`DiagnosticStatus.UNVERIFIABLE`	Analysis ran but proof was incomplete, timed out, or found a counterexample.
`DiagnosticStatus.BLOCKED`	Verification could not be attempted (parse error, no functions, CrossHair missing).

Read the specific reason from result.developer_fields["constraint_id"].

Common `developer_fields` keys

Every result carries verification_mode so callers can tell a plain symbolic run from a bounded run:

Key	Type	Description
`constraint_id`	string	Structured reason code, e.g. `symbolic_verifier.counterexample_found`.
`verification_mode`	string	`"symbolic"` for standard runs, `"bounded_symbolic"` for `verify_bounded()`.
`advisory_checks`	array	Non-proof-bearing analysis attached for developer or auditor review. Never influences the verdict.

Method-specific keys (function counts, loop lists, budget estimates) are documented in the sections below.

Why `VERIFIED` is never emitted

CrossHair’s search is timeout-bounded, not a completeness proof. “No counterexample found” is not the same as “no counterexample exists,” so a clean run maps to UNVERIFIABLE with constraint_id = "symbolic_verifier.no_counterexample_found" — never to VERIFIED. The DiagnosticResult contract structurally requires a proof_ref for VERIFIED, and this engine has no proof artifact to bind. Downstream policy gates must reject UNVERIFIABLE results for control flow. Treat symbolic-execution output as a bug hunter, not an authority.

Symbolic verification

verify_code() walks the AST, extracts every function with type annotations, and runs CrossHair on each one.

result = verifier.verify_code(code)

if result.is_verified:
    ...  # Never happens for this engine — see above
else:
    reason = result.developer_fields["constraint_id"]
    checked = result.developer_fields["functions_checked"]
    verified = result.developer_fields["functions_verified"]
    issues = result.developer_fields["issues"]

developer_fields on verify_code() results:

Key	Description
`functions_discovered`	Total functions found in the source.
`functions_checked`	Functions actually submitted to CrossHair.
`functions_verified`	Functions CrossHair proved (no counterexample and no timeout).
`functions_skipped`	Functions with no type annotations.
`functions_unverifiable`	Functions that could not be proven (skipped, timed out, or errored).
`counterexamples_found`	Count of counterexample issues reported by CrossHair.
`timeouts_found`	Count of timeout issues.
`issues`	Per-function issue records with `type`, `function`, and `description`.

verify_code() no longer accepts check_assertions — the parameter was never wired up. The current signature is verify_code(self, code: str) -> DiagnosticResult. Passing extra keyword arguments raises TypeError.

Counterexample: division by zero

result = verifier.verify_code("""
def divide(a: int, b: int) -> float:
    return a / b
""")

result.status                                        # DiagnosticStatus.UNVERIFIABLE
result.developer_fields["constraint_id"]             # "symbolic_verifier.counterexample_found"
result.developer_fields["counterexamples_found"]     # 1
result.developer_fields["issues"][0]["type"]         # "counterexample"

Untyped function: fails closed

CrossHair requires type hints. Untyped functions are reported as skipped and unverifiable — the result cannot be is_verified: True.

result = verifier.verify_code("""
def add(a, b):
    return a + b
""")

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

See Symbolic execution limits for the full fail-closed matrix.

Contract verification

verify_function_contract() injects preconditions as assert statements and re-runs verify_code() against the decorated source.

result = verifier.verify_function_contract(
    code="""
def sqrt(x: float) -> float:
    return x ** 0.5
""",
    function_name="sqrt",
    preconditions=["x >= 0"],
    postconditions=["__return__ >= 0"],
)

The returned DiagnosticResult follows the same shape as verify_code(). Read result.developer_fields["issues"] to find failing assertions.

Safety property analysis

verify_safety_properties() scans the AST for division-by-zero and index-out-of-bounds hazards. It always returns UNVERIFIABLE (the check is advisory and does not prove the code is safe) with structured details in developer_fields.

result = verifier.verify_safety_properties("""
def divide(a: int, b: int) -> float:
    return a / b
""")

result.developer_fields["is_safe"]              # False
result.developer_fields["warnings"]             # 1
result.developer_fields["errors"]               # 0
result.developer_fields["issues"][0]["type"]    # "potential_division_by_zero"

The advisory_checks array carries a safety_properties entry with the same summary counts.

Bounded model checking

verify_bounded() transforms the source to inject loop counters and recursion-depth checks, then calls verify_code() on the rewritten source. Every result from this method sets verification_mode = "bounded_symbolic" and includes the applied bounds plus the underlying complexity analysis.

result = verifier.verify_bounded(
    code=code,
    loop_bound=50,
    recursion_depth=20,
)

result.developer_fields["verification_mode"]     # "bounded_symbolic"
result.developer_fields["bounds_applied"]        # {"loop_bound": 50, "recursion_depth": 20, "prioritized": True}
result.developer_fields["complexity_analysis"]   # {"loops": [...], "recursions": [...], ...}

If the bounded-model transform itself fails, verify_bounded() returns BLOCKED with constraint_id = "symbolic_verifier.bounds_transform_error" instead of silently falling back to the untransformed source. See Bounded model checking for configuration guidance and preset budgets.

Complexity analysis

analyze_complexity() counts loops, direct and mutual recursions, and maximum loop-nesting depth. The result is always UNVERIFIABLE — the analysis is advisory and produces no proof.

result = verifier.analyze_complexity("""
def bubble_sort(arr: List[int]) -> List[int]:
    n = len(arr)
    for i in range(n):
        for j in range(n - 1):
            if arr[j] > arr[j + 1]:
                arr[j], arr[j + 1] = arr[j + 1], arr[j]
    return arr
""")

result.developer_fields["total_loops"]              # 2
result.developer_fields["max_loop_depth"]           # 2
result.developer_fields["total_recursive_functions"] # 0
result.developer_fields["complexity_score"]         # 4
result.developer_fields["recommendation"]["risk_level"] # "medium"

Use recommendation to pick sensible bounds for a follow-up verify_bounded() call.

Verification budget

get_verification_budget() estimates the number of symbolic paths CrossHair would explore, so callers can decide whether to attempt verification or fall back to a cheaper check.

result = verifier.get_verification_budget(code, max_paths=1000)

result.developer_fields["estimated_paths"]    # e.g. 200
result.developer_fields["max_paths"]          # 1000
result.developer_fields["feasible"]           # True

Both this method and analyze_complexity() are advisory — treat their output as heuristics, not proof. The result carries an advisory_checks entry with the same summary details.

Migrating from the legacy dict API

Before v5.3.0, SymbolicVerifier methods returned ad-hoc dicts (result.verified, result["issues"], result["complexity"], and so on). v5.3.0 removes those return types entirely — every method now returns a DiagnosticResult. Update your call sites using the map below.

Field cheat sheet

Legacy field	Replacement
`result.verified`	`result.is_verified` (always `False` for this engine)
`result["status"]` (string)	`result.status` (`DiagnosticStatus` enum) and `developer_fields["constraint_id"]`
`result["message"]`	`result.agent_message`
`result["issues"]`	`result.developer_fields["issues"]`
`result["functions_checked"]`	`result.developer_fields["functions_checked"]`
`result["complexity"]` / `"loop_depth"` / `"recursive"`	`result.developer_fields["complexity_score"]`, `"max_loop_depth"`, `"total_recursive_functions"`
`result["is_safe"]`	`result.developer_fields["is_safe"]`
`result["bounds_applied"]`	`result.developer_fields["bounds_applied"]`
n/a	`result.developer_fields["verification_mode"]` — new, `"symbolic"` or `"bounded_symbolic"`
n/a	`result.proof_ref` — always `None` for this engine

Before

result = verifier.verify_code(code)

if result["status"] == "verified":
    admit(payload)
elif result["status"] == "counterexamples_found":
    for issue in result["issues"]:
        log(issue["description"])
else:
    reject(payload, reason=result["message"])

After

from qwed_new.core.diagnostics import DiagnosticStatus

result = verifier.verify_code(code)

# This engine never emits VERIFIED — treat every result as unverified for
# control flow, and use developer_fields for the specific reason.
reject(payload, reason=result.agent_message)

if result.status is DiagnosticStatus.UNVERIFIABLE:
    reason = result.developer_fields["constraint_id"]
    if reason == "symbolic_verifier.counterexample_found":
        for issue in result.developer_fields["issues"]:
            log(issue["description"])

Do not gate control flow on is_verified for symbolic-engine results — it is always False. Downstream authority checks must inspect result.proof_ref, which this engine intentionally leaves as None. See Verification Diagnostics for the full 3-layer contract.

Removed parameters

verify_code(code, check_assertions=...) — the parameter was never used. Remove it from your call sites; passing it now raises TypeError.

Language support

Language	Support level
Python	Full
JavaScript	Basic (coming)
TypeScript	Basic (coming)
SQL	Via SQL Engine

Next steps

Verification Diagnostics — the DiagnosticResult contract in depth
Symbolic execution limits — when CrossHair works, when it doesn’t, and how to bound it
SQL engine — verify SQL queries
Logic engine — verify logical constraints

Overview

Core Engines

Analysis Engines

Specialized Engines

Capabilities

Quick start

The `DiagnosticResult` contract

Status values

Common `developer_fields` keys

Why `VERIFIED` is never emitted

Symbolic verification

Counterexample: division by zero

Untyped function: fails closed

Contract verification

Safety property analysis

Bounded model checking

Complexity analysis

Verification budget

Migrating from the legacy dict API

Field cheat sheet

Before

After

Removed parameters

Language support

Next steps

​Capabilities

​Quick start

​The DiagnosticResult contract

​Status values

​Common developer_fields keys

​Why VERIFIED is never emitted

​Symbolic verification

​Counterexample: division by zero

​Untyped function: fails closed

​Contract verification

​Safety property analysis

​Bounded model checking

​Complexity analysis

​Verification budget

​Migrating from the legacy dict API

​Field cheat sheet

​Before

​After

​Removed parameters

​Language support

​Next steps

Capabilities

Quick start

The `DiagnosticResult` contract

Status values

Common `developer_fields` keys

Why `VERIFIED` is never emitted

Symbolic verification

Counterexample: division by zero

Untyped function: fails closed

Contract verification

Safety property analysis

Bounded model checking

Complexity analysis

Verification budget

Migrating from the legacy dict API

Field cheat sheet

Before

After

Removed parameters

Language support

Next steps