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.

Updated in v7.0.0 (breaking). The security-scanning path (CodeVerifier and SecureCodeExecutor, backing POST /verify/code) also returns DiagnosticResult now, and proven-unsafe code is reported as VERIFIED with a separate admission decision. See Security scanning below and the changelog.

The Code Engine uses CrossHair, a symbolic execution tool for Python, to search for counterexamples to code properties.

CrossHair imports the module it analyzes, which runs that module’s top-level code. QWED runs CrossHair only inside a hardened Docker container and never on the host. Without Docker or the sandbox image, verify_code() returns BLOCKED with constraint_id = "symbolic_verifier.runtime_unavailable". See Docker sandbox requirement.

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

Prerequisites

Install the symbolic extra, which includes CrossHair and the docker client, then build the sandbox image from a qwed-verification checkout:

pip install "qwed[symbolic]"
docker build -t qwed-crosshair-sandbox:0.0.101 docker/crosshair-sandbox

The image is built from docker/crosshair-sandbox/Dockerfile. QWED never pulls it at runtime. Set QWED_CROSSHAIR_IMAGE to use a different tag.

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, code over 120 KiB, Docker sandbox unavailable).

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 inside the Docker sandbox. QWED addresses each function by module qualname (target.func or target.Class.method). Functions nested inside other functions can’t be loaded by name and are reported as unverifiable.

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.

Security scanning (`CodeVerifier`)

Separate from symbolic execution, CodeVerifier scans code for security vulnerabilities using AST and pattern analysis. It backs POST /verify/code and the CODE item type in batch verification. As of v7.0.0, verify_code(), verify_python_deep(), and verify_batch() return a DiagnosticResult.

Status semantics: `VERIFIED` is truth, not admission

Outcome	`status`	`developer_fields`	`proof_ref`
Safe code	`VERIFIED`	`is_valid: true`, `is_safe: true`, `constraint_id: "code_verifier.code_safe"`	Present
Unsafe code	`VERIFIED` (as-unsafe)	`is_valid: false`, `is_safe: false`, `critical_count`, `issues`	Present
Empty code or non-string `language`	`BLOCKED`	`constraint_id: "code_verifier.unsupported_language"`	`null`
Python that does not parse	`BLOCKED`	`constraint_id: "code_verifier.parse_error"`	`null`
Internal error	`BLOCKED`	`constraint_id: "code_verifier.execution_error"`	`null`

Proving that a snippet is unsafe is a successful proof, so unsafe code is VERIFIED, never BLOCKED. BLOCKED is reserved for cases where verification itself failed, and blocked results carry no proof_ref.

Never treat status == "VERIFIED" as “safe to execute”. Admission is a separate decision: POST /verify/code attaches an explicit admission field (ADMIT or BLOCKED), and developer_fields.is_valid is the safety gate. Gate execution on admission or is_valid, not on status.

Shell and process execution is never admitted

CodeVerifier reports any shell or process execution as a CRITICAL issue with type process_execution, so the snippet is unsafe (is_valid: false) and POST /verify/code returns admission: BLOCKED. This applies even when the command is a constant. The following calls are covered:

os.system, os.popen, os.startfile
The os.exec*, os.spawn*, and os.posix_spawn* families
os.fork, os.forkpty, and pty.fork
subprocess.*
pty.spawn
asyncio.create_subprocess_*
Dynamic import and execution: importlib.import_module, importlib.__import__, runpy.run_module, and runpy.run_path
Native library loaders: ctypes.CDLL, ctypes.cdll, ctypes.WinDLL, ctypes.windll, ctypes.OleDLL, ctypes.oledll, and ctypes.PyDLL
Any call on the raw OS backend modules posix and nt

Calls made through an aliased import are detected too, for example import subprocess as sp, from os import system as run_it, or from os import *. verify_code(), verify_python_deep(), and POST /verify/code all apply this rule.

from qwed_new.core.code_verifier import CodeVerifier

code_verifier = CodeVerifier()
result = code_verifier.verify_code(
    "import subprocess as sp\nsp.run(['ls', '-la'])",
    language="python",
)
print(result.developer_fields["is_valid"])     # False
print(result.developer_fields["issues"])
# [{"severity": "CRITICAL", "type": "process_execution", ...}]

If generated code needs to run commands, route them through a reviewed, sandboxed tool instead.

Before v7.2.3, shell and subprocess calls were warnings and the code was admitted. See GHSA-6rxr-gq43-694g. Before v7.3.0, fork, dynamic import, ctypes loaders, posix/nt, and file and network access were warnings or undetected and the code was admitted. See GHSA-4phf-6h72-9xfg.

`eval`, `exec`, and `compile` are matched as names

CodeVerifier reports eval, exec, compile, __import__, getattr, and setattr as a CRITICAL issue with type dangerous_function. The verifier matches these names on the Python AST, not as substrings of a line. Longer identifiers that only contain them are not flagged, except that any line containing __import__ is still reported as dangerous_attribute. Common safe calls are admitted:

cur.execute("SELECT ?", params), which is parameterised SQL
model.evaluate(x, y) and model.evaluate(ds, verbose=0)
re.compile(r"[0-9]+") in a snippet that has import re. Without the import in the snippet, re.compile is refused, because the verifier can’t tell that re is the standard module
compile_report(), and the names inside longer words in strings and comments, such as "executing job"

The matching is still strict where a name can reach the builtin another way. The verifier refuses the names when used as a value (f = eval), as a keyword argument, as a parameter or function name, in an import, as an attribute, or as a whole identifier in a string. It also follows names built from literals with + or %, such as "ex" + "ec". It doesn’t follow names built with join or chr. Longer helpers that run code or start a process, such as exec_module and the os.exec* family, stay refused. model.eval(), model.evaluate(x), and model.evaluate() stay refused too. ast.literal_eval is admitted.

result = code_verifier.verify_code(
    "cur.execute('SELECT * FROM users WHERE id = ?', (user_id,))",
    language="python",
)
print(result.developer_fields["is_valid"])     # True

result = code_verifier.verify_code("f = eval\nf(user_input)", language="python")
print(result.developer_fields["is_valid"])     # False
print(result.developer_fields["issues"])
# [{"severity": "CRITICAL", "type": "dangerous_function", ...},
#  {"severity": "CRITICAL", "type": "builtin_not_admitted", ...}]   # second issue from v9.1.0

Python that does not parse is BLOCKED with constraint_id: "code_verifier.parse_error", because the AST checks cannot run on it.

Before v9.0.0, the verifier matched these names anywhere in a line, so cur.execute(...), model.evaluate(...), and re.compile(...) were refused as dangerous_function. Python that did not parse was reported safe unless a line matched one of the patterns.

File and network access is never admitted

CodeVerifier reports file system and network I/O that the code itself calls as a CRITICAL issue with type file_or_network_access, so the snippet is unsafe (is_valid: false) and POST /verify/code returns admission: BLOCKED. The following are covered, including through aliased imports:

The bare open() builtin and io.open
shutil.*, pathlib.Path, and file-mutating os calls such as os.remove, os.rename, os.mkdir, os.chmod, and os.open
socket.socket, socket.create_connection, and socket.create_server
urllib.request, http.client, requests.*, httpx.*, aiohttp.*, and asyncio.open_connection
ftplib, smtplib, telnetlib, poplib, and imaplib

This check doesn’t flag os.path.*. The string helpers such as os.path.join and os.path.basename are admitted. From v9.1.0, the os.path functions that read the file system, such as os.path.exists, os.path.isfile and os.path.getsize, are refused by the allowlist (attribute_not_admitted); see Only listed modules, builtins and attributes are admitted.

result = code_verifier.verify_code(
    "data = open('/etc/passwd').read()",
    language="python",
)
print(result.developer_fields["is_valid"])     # False
# [{"severity": "CRITICAL", "type": "file_or_network_access", ...}]

These checks cover calls the code makes by name. They don’t see the objects your executor puts in the code’s namespace: see the note under Only listed modules, builtins and attributes are admitted. If generated code needs to read files or call the network, route that I/O through a reviewed, sandboxed tool.

Only listed modules, builtins and attributes are admitted

Changed in v9.1.0 (GHSA-9r7q-mx75-hcj7)

CodeVerifier admits Python code only when everything it uses is on QWED’s lists. Lists of dangerous calls can’t be complete: before v9.1.0, code that used io.FileIO, urllib3, pickle.Unpickler, multiprocessing or os.environ was VERIFIED · ADMIT. Python code is now admitted only when all of the following hold:

Every module it imports, and every name it uses from that module, is on the list. The list holds standard-library modules that compute without files, the network, processes, the environment or the import system, such as math, json, re, datetime, decimal, collections and itertools. Third-party modules, such as numpy, pandas and requests, are not admitted, and nor are asyncio, logging, subprocess, importlib or pathlib. An import is refused even if the code calls nothing from the module.
Every builtin it reads is listed. A read of open, eval, exec, compile, __import__, vars, globals, locals, getattr, setattr, delattr, help, license, credits, copyright, breakpoint, memoryview or __build_class__ is refused, also where the name is the code’s own variable or parameter. Rename the variable, for example to help_text. print, input, exit and quit are admitted.
Every special attribute (__x__) it uses is listed. The protocol methods, such as __init__, __len__ and __eq__, and plain data, such as __name__ and __doc__, are listed. Attributes such as __func__, __wrapped__, __get__, __getstate__, __reduce__, __dict__ and __class__ are refused.
It reads no attribute’s value by a name made at run time. hasattr(obj, name) is admitted: it only answers whether the attribute exists, although the lookup can run a property. .format and .format_map need a template written in the code with no attribute in a field, such as "{} items".format(n). Use an f-string otherwise. A class pattern with positional parts, such as case Point(x, y), needs a class whose __match_args__ is fixed.
It uses no module as a value (m = json), writes to no module (json.dumps = f), and reads no frame or traceback.

Admission checks the code’s text, not the objects your executor puts in its namespace. A name the code uses but doesn’t define, such as f in f("/etc/passwd"), isn’t checked, so if your executor binds f to open, admitted code can read files. Expose only the objects and callables the code needs. Each refusal is a CRITICAL issue that names the module, builtin or attribute in its pattern. The issue type is one of module_not_admitted, attribute_not_admitted, module_reference, module_write, builtin_not_admitted, special_attribute, frame_introspection or dynamic_lookup.

from qwed_new.core.code_verifier import CodeVerifier

code_verifier = CodeVerifier()
result = code_verifier.verify_code("import numpy as np\nprint(np.mean([1, 2, 3]))", language="python")
print(result.developer_fields["is_valid"])     # False
# [{"severity": "CRITICAL", "type": "module_not_admitted", "pattern": "numpy", ...}]

result = code_verifier.verify_code("import math\nprint(math.sqrt(16))", language="python")
print(result.developer_fields["is_valid"])     # True

Upgrading to v9.1.0. POST /verify/code, QWEDLocal.verify_code and the CLI can refuse code that v9.0.0 admitted. Read the issues on the result: each one names what to remove or replace.

Trusted modules

CodeVerifier(trusted_modules=...) takes top-level module names that your own runtime confines, such as a sandbox with its own import guard. Code may use a trusted module although it is not on the list, also as a value or by writing to it. The allowlist’s module checks skip a trusted module, so don’t rely on them for one. The checks from earlier releases still apply to it, such as the code-running modules and file, network and process calls: CodeVerifier(trusted_modules=["timeit"]) still refuses import timeit. The builtin, attribute and frame checks also still apply.

from qwed_new.core.code_verifier import CodeVerifier

sandbox_verifier = CodeVerifier(trusted_modules=["numpy", "pandas"])

QWED’s code-execution sandbox passes numpy, pandas, scipy, sklearn, statsmodels and patsy as trusted, so the Stats engine still runs code that uses them.

Code hidden from the checks is refused

Changed in v9.0.0

Before v9.0.0, the following code was VERIFIED · ADMIT because the checks never saw what it ran. It is now refused:

Modules taken by name from the import system (GHSA-qrp4-p44j-m484): __loader__.load_module(...), importlib.util.module_from_spec, the importlib bootstrap, pkgutil.resolve_name, pydoc.locate, and any read of sys.modules.
Modules that run strings as code (GHSA-jrxf-9jh4-86w7): importing timeit, cProfile, profile, pdb, bdb, code, codeop, trace, doctest, logging.config or idlelib. File readers such as tarfile, zipfile, codecs.open, linecache, fileinput, glob, tempfile, sqlite3, shelve and dbm are file access.
Code in strings that typing evaluates (GHSA-p75q-7rg5-ff46): string annotations and ForwardRef strings that hold a call, lambda, comprehension or assignment expression. __forward_code__, __forward_arg__, __annotations__ and __annotate__ are dangerous attributes.
A source encoding other than UTF-8 (GHSA-pr6c-cqg8-6w5r): under a utf-7 or unicode_escape coding declaration, text checked as a comment can decode to statements when the code runs. A coding declaration whose codec is not UTF-8 is a CRITICAL issue of type source_encoding. Save the file as UTF-8, then remove the declaration or declare utf-8.

SDK clients use `CodeVerifier`, not `CodeGuard`

As of v8.0.0, QWEDClient.verify_code always calls POST /verify/code, so CodeVerifier decides admission. When the server can’t be reached, the client returns UNVERIFIABLE. QWEDLocal.verify_code runs CodeVerifier in process. The CodeGuard blocklist is a pre-filter only. It blocks reflective calls, __builtins__, dunder attributes, importlib, builtins, ctypes, marshal, and dotted imports, and it marks its own pass as advisory. See GHSA-4rj3-8wqj-cqwc and GHSA-v8qq-v427-qrqc.

Hardcoded OpenAI keys

The code verifier flags hardcoded OpenAI API keys, including project-scoped (sk-proj-), service-account (sk-svcacct-), and admin (sk-admin-) keys as well as legacy sk- keys. Detection of the scoped formats was added in v7.2.3 (GHSA-64xf-wffc-63fm).

Batch verification

verify_batch() returns a single DiagnosticResult with per-item verdicts, a summary (safe / unsafe / blocked counts and total_critical), and an overall is_valid. is_valid is true only when all snippets are safe — a batch with any unsafe or blocked item is non-admissible.

`SecureCodeExecutor` dangerous-pattern gate

SecureCodeExecutor.execute() no longer admits execution on the verifier verdict alone. It applies an unconditional OWASP LLM06 dangerous-pattern gate (os., sys., subprocess, __import__, eval, exec, compile, open(, socket, urllib, requests, http, and similar) and blocks execution with CONSTRAINT_DANGEROUS_PATTERN. The scan is AST-aware: it matches actual executable operations (imports, attribute access, calls), so dangerous keywords appearing only in comments, docstrings, or string literals do not cause false denials. The advisory-only fallback is retained only when verification itself fails closed.

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

Prerequisites

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

Security scanning (`CodeVerifier`)

Status semantics: `VERIFIED` is truth, not admission

Shell and process execution is never admitted

`eval`, `exec`, and `compile` are matched as names

File and network access is never admitted

Only listed modules, builtins and attributes are admitted

Trusted modules

Code hidden from the checks is refused

SDK clients use `CodeVerifier`, not `CodeGuard`

Hardcoded OpenAI keys

Batch verification

`SecureCodeExecutor` dangerous-pattern gate

Language support

Next steps

​Capabilities

​Prerequisites

​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

​Security scanning (CodeVerifier)

​Status semantics: VERIFIED is truth, not admission

​Shell and process execution is never admitted

​eval, exec, and compile are matched as names

​File and network access is never admitted

​Only listed modules, builtins and attributes are admitted

​Trusted modules

​Code hidden from the checks is refused

​SDK clients use CodeVerifier, not CodeGuard

​Hardcoded OpenAI keys

​Batch verification

​SecureCodeExecutor dangerous-pattern gate

​Language support

​Next steps

Capabilities

Prerequisites

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

Security scanning (`CodeVerifier`)

Status semantics: `VERIFIED` is truth, not admission

Shell and process execution is never admitted

`eval`, `exec`, and `compile` are matched as names

File and network access is never admitted

Only listed modules, builtins and attributes are admitted

Trusted modules

Code hidden from the checks is refused

SDK clients use `CodeVerifier`, not `CodeGuard`

Hardcoded OpenAI keys

Batch verification

`SecureCodeExecutor` dangerous-pattern gate

Language support

Next steps