Math engine - QWED Documentation

The Math Engine is QWED’s core verification engine. It uses SymPy for symbolic computation to provide exact verification of mathematical claims.

Capabilities

Category	Examples	Method
Arithmetic	`2+2=4`, `15*3=45`	SymPy exact
Algebra	`x^2 - 1 = (x-1)(x+1)`	SymPy `simplify`
Calculus	Derivatives, integrals, limits	SymPy symbolic
Trigonometry	`sin(π/2) = 1`, `cos(0) = 1`	SymPy symbolic
Logarithms	`log(e) = 1`, `ln(e^x) = x`	SymPy symbolic
Financial	Compound interest, NPV, IRR	mpmath + formulas
Statistics	Mean, std dev, percentiles	NumPy / SymPy stats

Quick start

from qwed_sdk import QWEDClient

client = QWEDClient(api_key="your_key")

# Verify a math claim
result = client.verify_math("15% of 200 is 30")
print(result.verified)  # True
print(result.status)    # "VERIFIED"

Core operations

1. Expression evaluation

Verify that an expression equals a value:

# Simple arithmetic
result = client.verify_math("2 * (5 + 10) = 30")
# ✓ Verified

# Complex expression
result = client.verify_math("sqrt(16) + 3^2 = 13")
# ✓ Verified

# Percentage
result = client.verify_math("15% of 200 = 30")
# ✓ Verified

2. Identity verification

Check if two expressions are mathematically equivalent:

# Algebraic identity - TRUE
result = client.verify_math("(a+b)^2 = a^2 + 2*a*b + b^2")
# ✓ Verified: Algebraic identity proven

# Algebraic identity - FALSE
result = client.verify_math("(a+b)^2 = a^2 + b^2")
# ✗ Proven false: VERIFIED with is_valid false, admission DENY

# Trig identity
result = client.verify_math("sin(x)^2 + cos(x)^2 = 1")
# ✓ Verified: Pythagorean identity

Identity verification uses symbolic simplification first. If SymPy proves the identity algebraically, the result is VERIFIED. When symbolic simplification is inconclusive, the engine samples five test points as a fallback. Only points that the engine can successfully evaluate count toward agreement — the engine skips domain-restricted expressions (e.g., log(x) at x = -1) rather than producing a false negative.

Numerical sampling cannot prove equivalence. If all sample points agree but no formal proof was established, the engine now fails closed — returning BLOCKED with is_equivalent: false, method: "numerical_sampling_rejected", and confidence: 0.0. Two expressions can match at fixed points without being algebraically identical, so sampling-only agreement is rejected outright. Treat BLOCKED results as unverified.

Domain-restricted identities

An identity that holds only after SymPy cancels a removable singularity is not proven. For example, x/x = 1 is false at x = 0, and (x**2-1)/(x-1) = x+1 is false at x = 1. The engine reads the denominators from the expression before SymPy simplifies it. It returns VERIFIED only when both sides have the same singular factors.

POST /verify/math returns UNVERIFIABLE with constraint_id: "math.domain_restricted_identity" and admission BLOCKED.
verify_identity returns status: "INCONCLUSIVE" with reason: "domain_mismatch" and the same constraint_id.

The same rule covers floor division and modulo (x//x = 1, x % x = 0). An identity with a free symbol that uses a function with poles or singular points (tan, sec, log, factorial) is never verified this way. Closed constants such as factorial(5) = 120 still verify.

result = client.verify_math("x/x = 1")
# result.status == "UNVERIFIABLE"
# constraint_id == "math.domain_restricted_identity"

3. Derivatives

Verify calculus derivatives:

result = client.verify_derivative(
    expression="x^3 + 2*x^2",
    variable="x",
    expected="3*x^2 + 4*x"
)
# ✓ Verified

# Higher-order derivatives
result = client.verify_derivative(
    expression="x^4",
    variable="x",
    expected="12*x^2",
    order=2  # Second derivative
)
# ✓ Verified

Derivatives in `/verify/math` identities

Changed in v9.0.0

POST /verify/math and /verify/batch math items evaluate diff and Derivative inside an identity, so you can state a derivative claim directly. == reads as =.

client.verify_math("diff(x**2, x) == 2*x")
# ✓ VERIFIED, is_valid true, admission ADMIT

client.verify_math("diff(x**3, x, 2) = 6*x")
# ✓ VERIFIED (second derivative)

client.verify_math("diff(sqrt(x), x)*2*sqrt(x) = 1")
# UNVERIFIABLE, constraint_id "math.domain_restricted_identity"

Order limit. The total derivative order in one expression is at most 3, nested calls included. Each order multiplies the work that simplification has to do.
No derivative inside a power, factorial, or binomial. diff(x**2, x)**2 is refused. A reciprocal or a root, such as 2*x/diff(x**2, x) or sqrt(diff(x**2, x)), is allowed.
Domain check. The domain check reads each evaluated derivative as well as the text. A derivative can be undefined where the expression it differentiates is defined. diff(sqrt(x), x) = 1/(2*sqrt(x)) is VERIFIED, but diff(sqrt(x), x)*2*sqrt(x) = 1 holds only for x other than 0, so it is UNVERIFIABLE with math.domain_restricted_identity.

Leibniz notation is refused, not read as symbols. d/dx(x^2) = 2x, dy/dx, d(x^2)/dx, dy/dtheta, and d^2y/dx^2 return BLOCKED with constraint_id: "math.parse_error" and the message to write diff(f, x). Write diff(x^2, x) = 2*x instead.The same refusal covers a name starting with d that SymPy splits into letters, because it would be read as d times the rest: dx, dtheta, d2y, and also data (read as a**2*d*t). A name the parser already knows, such as delta, diff, or a symbol you declare, is never refused. To use a d-prefixed name as a symbol, pass it in extra_symbols. extra_symbols is an argument of safe_parse_expr() in the Python package only; /verify/math and batch items don’t take it, so there rename the variable. A name with _, such as distance_m, is a symbol unless the rest is a variable used beside it (dx_1 beside x_1).

Parse errors

Changed in v9.0.0

Input the parser refuses is BLOCKED with constraint_id: "math.parse_error" and the message Expression could not be parsed, as SQL and schema parse errors are. Leibniz notation gets the diff(f, x) message instead. The parser’s own error text is not returned. Before v9.0.0, such input returned BLOCKED with api.math.execution_error and Internal verification error. A /verify/batch math item the parser refuses gets the same BLOCKED result instead of a failed item.

4. Integrals

Verify indefinite and definite integrals:

# Indefinite integral
result = client.verify_integral(
    expression="2*x",
    variable="x",
    expected="x^2"  # + C implied
)
# ✓ Verified

# Definite integral
result = client.verify_integral(
    expression="x^2",
    variable="x",
    lower=0,
    upper=1,
    expected="1/3"
)
# ✓ Verified

5. Limits

result = client.verify_limit(
    expression="sin(x)/x",
    variable="x",
    point=0,
    expected=1
)
# ✓ Verified: lim(x→0) sin(x)/x = 1

Financial calculations

Compound interest

result = client.verify_compound_interest(
    principal=1000,
    rate=0.05,      # 5% annual
    time=10,        # years
    n=12,           # monthly compounding
    expected=1647.01
)
# ✓ Verified

Net present value (NPV)

result = client.verify_npv(
    rate=0.10,
    cash_flows=[-1000, 300, 400, 500, 600],
    expected=388.07
)
# ✓ Verified

Internal rate of return (IRR)

result = client.verify_irr(
    cash_flows=[-1000, 400, 400, 400],
    expected=0.0985  # ~9.85%
)
# ✓ Verified

Cash flows with more than one sign change, or that fail to converge, are now rejected with BLOCKED rather than returning a best-effort iterate. See verify_irr — convergence proof for the full state table.

Verdicts and admission

The math engine separates the verdict (did the engine decide the claim?) from admission (may you use the result?). A claim the engine proves false is a decided verdict. It is VERIFIED with is_valid: false and admission DENY, never UNVERIFIABLE. Gate on admission, not on the verdict alone.

Outcome	Example	Legacy engine status	Verdict	`is_valid`	Admission
Proven true	`2+2=4`	`VERIFIED`	`VERIFIED`	`true`	`ADMIT`
Proven false	`2+2=5`, `(a+b)^2 = a^2 + b^2`	`DISPROVEN`	`VERIFIED`	`false`	`DENY`
Undecided	Symbolic difference SymPy can’t decide, float rounding residue, non-finite value	`INCONCLUSIVE`	`UNVERIFIABLE`	`false`	`DENY`
Domain-restricted identity	`x/x = 1`, `diff(sqrt(x), x)2sqrt(x) = 1`	`INCONCLUSIVE`	`UNVERIFIABLE`	`false`	`DENY`
Undefined part	`log(0)**0 = 2`	n/a	`UNVERIFIABLE` (`math.undefined_part`)	`false`	`DENY`
Parse error	`d/dx(x^2) = 2x`, unparseable text	n/a	`BLOCKED` (`math.parse_error`)	`false`	`DENY`
Verification failed	Invalid input, units of different dimensions	`BLOCKED`	`BLOCKED`	`false`	`DENY`

The legacy engine status is the status field of the dictionary that VerificationEngine methods return. HTTP responses report admission DENY as "admission": "BLOCKED". POST /verify/math and /verify/batch math items build the identity verdict with the same function, so both routes return the same verdict for the same claim. A claim with a side that has an undefined part is not disproven. SymPy evaluates some undefined parts away: log(0)**0 becomes 1, so log(0)**0 = 2 looks like 1 = 2. A part is undefined when it evaluates to zoo or nan. A symbol-free part is also undefined when it is not finite. Such a claim is UNVERIFIABLE with constraint_id: "math.undefined_part" and no attestation. log(0)**0 = 1, where the sides agree, is UNVERIFIABLE with math.domain_restricted_identity. x/x = 2 and 2x^2 = 5 are still disproven.

VerificationEngine no longer emits CORRECTION_NEEDED. A mismatch decided by a concrete computation now returns DISPROVEN. If your code branches on status == "CORRECTION_NEEDED", switch to DISPROVEN for engine dictionaries, or to admission and is_valid for API responses.

The engine returns DISPROVEN only when the mismatch is decided:

Symbolic checks. Derivatives, indefinite integrals, limits, and /verify/math identities are disproven only when SymPy decides the difference is non-zero. The difference can be decided outright, through the coefficients of a bounded polynomial, or at an exact witness point inside each symbol’s declared domain. Otherwise the result is INCONCLUSIVE.
Float residue. A non-zero difference that comes from a float literal (0.1 + 0.2 = 0.3 leaves 5.55e-17) is INCONCLUSIVE, not DISPROVEN.
Non-finite values. A mismatch involving an overflowed value or a NaN claim is INCONCLUSIVE.
Exact matrices and scalars. Matrix add, multiply, inverse, transpose, and determinant read each float input as the decimal you wrote (0.1 is 1/10), so [[0.1]] + [[0.2]] vs [[0.3]] is VERIFIED. A claim inside the float rounding window is INCONCLUSIVE. A claimed matrix of the wrong shape is DISPROVEN.
Unit conversion. verify_unit_conversion uses exact unit definitions (1 lb = 0.45359237 kg, 1 US gal = 3.785411784 L). Converting between units of different dimensions, such as m to kg, returns BLOCKED instead of comparing the numbers.

from qwed_new.core.verifier import VerificationEngine

engine = VerificationEngine()

engine.verify_math("2+2", 5)["status"]       # "DISPROVEN"
engine.verify_math("2+2", 4)["status"]       # "VERIFIED"
engine.verify_unit_conversion(1, "m", "kg", 1)["status"]  # "BLOCKED"

Fail-closed semantics

Three verification methods require an additional proof step before returning VERIFIED. When the underlying claim is ambiguous, incomplete, or numerically unproven, the engine returns BLOCKED or DISPROVEN with structured diagnostics rather than a best-effort answer.

`verify_statistics(statistic="mode")` — unique mode required

mode verification returns VERIFIED only when a single value has the maximum frequency. When two or more values tie for the maximum frequency, the engine returns BLOCKED with an ambiguous_modes list — it will not heuristically pick one.

Condition	Status	Notes
Exactly one value at max frequency, claim matches	`VERIFIED`	Unique mode
Exactly one value at max frequency, claim differs	`DISPROVEN`	`calculated` returned
Two or more values tied at max frequency	`BLOCKED`	`ambiguous_modes` returned; result is independent of the claimed value
All values equal (e.g., [5, 5, 5])	`VERIFIED` (if claim matches)	Single distinct value at max frequency � unique mode

Response fields on the BLOCKED case:

Field	Type	Description
`status`	string	`"BLOCKED"`
`error`	string	Human-readable message including the tied mode count and frequency
`statistic`	string	`"mode"`
`data_points`	integer	Number of observations
`ambiguous_modes`	list	Sorted list of all values tied at the maximum frequency

# BLOCKED — two values tied at max frequency
result = client.verify_statistics(
    statistic="mode",
    data=[1, 1, 2, 2, 3],
    expected=1,
)
# result["status"] == "BLOCKED"
# result["ambiguous_modes"] == [1, 2]
# result["error"].startswith("Ambiguous mode: 2 values share the maximum frequency")

# VERIFIED — unique mode
result = client.verify_statistics(
    statistic="mode",
    data=[1, 1, 2, 3],
    expected=1,
)
# result["status"] == "VERIFIED"

The Stats Engine’s compute_statistics method returns an equivalent multimodal error on its own surface — see Stats engine — Error handling.

`verify_matrix_operation(operation="eigenvalues")` — cardinality match required

Eigenvalue verification requires the claimed list to have the same length as the calculated eigenvalue set, counting algebraic multiplicity. Previously the value comparison used zip, which silently truncated to the shorter list — so a claim of [2] for a matrix with eigenvalues [2, 3] could pass. The cardinality check now runs before the value comparison.

Condition	Status	Notes
`len(claimed) == len(calculated)` and all values match	`VERIFIED`	Full agreement
`len(claimed) == len(calculated)` and any value differs	`DISPROVEN`	Values compared as complex numbers after sorting
`len(claimed) != len(calculated)` (under- or over-complete)	`DISPROVEN`	`calculated_count` and `claimed_count` returned

Response fields on the cardinality-mismatch case:

Field	Type	Description
`status`	string	`"DISPROVEN"`
`error`	string	Message noting the mismatch and that all eigenvalues, including repeated roots, must be specified
`calculated_eigenvalues`	list	Full eigenvalue list computed by SymPy (expanded by algebraic multiplicity)
`claimed_eigenvalues`	list	The list you submitted
`calculated_count`	integer	Length of `calculated_eigenvalues`
`claimed_count`	integer	Length of `claimed_eigenvalues`

# DISPROVEN — claim omits the second eigenvalue
result = client.verify_matrix_operation(
    operation="eigenvalues",
    matrix=[[2, 0], [0, 3]],
    expected=[2],
)
# result["status"] == "DISPROVEN"
# result["calculated_count"] == 2
# result["claimed_count"] == 1
# result["calculated_eigenvalues"] == [2.0, 3.0]

# DISPROVEN — repeated root must be listed twice
result = client.verify_matrix_operation(
    operation="eigenvalues",
    matrix=[[2, 0], [0, 2]],
    expected=[2],
)
# result["status"] == "DISPROVEN"
# result["calculated_eigenvalues"] == [2.0, 2.0]

# VERIFIED — full list including multiplicity
result = client.verify_matrix_operation(
    operation="eigenvalues",
    matrix=[[2, 0], [0, 2]],
    expected=[2, 2],
)
# result["status"] == "VERIFIED"

`verify_irr` — convergence proof

IRR verification now requires proof that Newton-Raphson converged before returning VERIFIED. Successful results include converged: true and iterations_used for auditability. The engine blocks inputs whose IRR is mathematically ambiguous or numerically unreachable rather than returning the current iterate.

Condition	Status	Notes
Converged and claimed IRR matches within `tolerance`	`VERIFIED`	`converged: true`, `iterations_used` returned
Converged and claimed IRR differs by more than `tolerance`	`DISPROVEN`	`calculated_irr` returned
All cash flows are zero	`BLOCKED`	IRR is undefined — any rate satisfies `NPV = 0`
Zero sign changes (all cash flows same sign)	`BLOCKED`	No real IRR exists (Descartes’ rule)
More than one sign change in cash flows	`BLOCKED`	Multi-root ambiguity — multiple real IRRs may exist
Derivative reaches zero mid-iteration	`BLOCKED`	Newton-Raphson stalled — cannot proceed from this path
Did not converge within 100 iterations	`BLOCKED`	`iterations_used: 100`, residual reported in `error`

Response fields:

Field	Type	Description
`status`	string	`"VERIFIED"`, `"DISPROVEN"`, or `"BLOCKED"`
`converged`	boolean	`true` only on successful convergence (present on `VERIFIED`)
`iterations_used`	integer	Newton-Raphson iterations run (present on `VERIFIED` and iteration-related `BLOCKED` cases)
`calculated_irr`	float	Present when Newton-Raphson converged
`claimed_irr`	float	The value you submitted (present when converged)
`sign_changes`	integer	Present on sign-change `BLOCKED` cases
`cash_flows`	list	Echoed on `BLOCKED` cases for auditability

# VERIFIED — single sign change, Newton converges
result = client.verify_irr(
    cash_flows=[-1000, 400, 400, 400],
    expected=0.0985,
)
# result["status"] == "VERIFIED"
# result["converged"] is True
# result["iterations_used"] <= 100

# BLOCKED — multi-root ambiguity (two sign changes)
result = client.verify_irr(
    cash_flows=[-100, 230, -132],
    expected=0.10,
)
# result["status"] == "BLOCKED"
# result["sign_changes"] == 2

# BLOCKED — zeros do not hide real sign transitions
result = client.verify_irr(
    cash_flows=[-100, 0, 230, -132],
    expected=0.10,
)
# result["status"] == "BLOCKED"
# result["sign_changes"] == 2

# BLOCKED — all cash flows are zero, IRR undefined
result = client.verify_irr(
    cash_flows=[0, 0, 0],
    expected=0.0,
)
# result["status"] == "BLOCKED"
# result["error"].startswith("IRR is undefined")

# BLOCKED — all same-sign cash flows, no real IRR exists
result = client.verify_irr(
    cash_flows=[100, 200, 300],
    expected=0.10,
)
# result["status"] == "BLOCKED"
# result["sign_changes"] == 0

These three methods are behavior changes. Inputs that previously received VERIFIED — an ambiguous mode dataset, an under-specified eigenvalue list, or a cash-flow series with multiple sign changes — now return BLOCKED or DISPROVEN. Treat both statuses as not admitted and consume the structured diagnostic fields rather than relying on a numeric result.

Trust boundary

When you verify a natural language math query through the /verify/natural_language endpoint, the engine only decides the expression the LLM translated your question into. The response carries the enforced verdict for that expression, the scope it covers, and a separate admission decision.

{
  "status": "VERIFIED",
  "is_valid": true,
  "translated_expression": "0.15 * 200",
  "verification_scope": "translated_expression_only",
  "query_semantics_verified": false,
  "admission": "BLOCKED"
}

Admission is always BLOCKED (DENY) for natural language queries, even when the translated claim holds, because nothing proves the translation means what you asked. A translated claim proven false is VERIFIED with is_valid: false. The control plane also records a trust_boundary object that describes exactly what the pipeline proved and what it did not:

{
  "trust_boundary": {
    "query_interpretation_source": "llm_translation",
    "query_semantics_verified": false,
    "verification_scope": "translated_expression_only",
    "deterministic_expression_evaluation": true,
    "formal_proof": false,
    "translation_claim_self_consistent": true,
    "provider_used": "openai_compat",
    "overall_status": "VERIFIED"
  }
}

Field	Meaning
`query_interpretation_source`	How the user query was converted to an expression (always `llm_translation`)
`query_semantics_verified`	Whether the translation accurately represents the user’s intent (`false` — this is not formally provable)
`verification_scope`	What was actually verified (`translated_expression_only`)
`deterministic_expression_evaluation`	Whether the expression itself was evaluated deterministically
`formal_proof`	Whether a formal proof was established
`translation_claim_self_consistent`	Whether the LLM’s claimed answer matches the computed answer
`overall_status`	The response-level status reflecting the trust boundary

QWED evaluates the translated expression deterministically, but it cannot verify that the LLM correctly interpreted your intent. That is why admission is always BLOCKED for natural language queries. Use POST /verify/math directly when you need an admissible result.

Error handling

When verification fails, QWED provides detailed error information:

result = client.verify_math("15% of 200 = 40")

if not result.verified:
    print(result.error)
    # "Calculation incorrect: 15% of 200 = 30, not 40"
    print(result.expected)
    # 30
    print(result.actual)
    # 40

Exact SymPy arithmetic

When SymPy is available, the math engine evaluates expressions using SymPy-native types (sympy.Integer, sympy.Float) instead of Python built-in int and float. This prevents floating-point drift during intermediate computation and ensures that comparisons between LLM answers and verified results use symbolic simplification rather than string matching alone.

Decimal precision

The math engine accepts Decimal values for exact arithmetic, which is especially useful for financial calculations:

from decimal import Decimal

result = client.verify_math(
    expression="0.1 + 0.2",
    expected_value=Decimal("0.3")  # Exact comparison, no float drift
)
# ✓ Verified

When use_decimal=True (the default), the engine uses Decimal internally regardless of whether you pass a float or Decimal.

Float precision advisory

When an expression submitted to POST /verify/math contains binary floating-point constants (0.1, 1e9, 1.0j), the response carries a precision advisory in developer_fields.advisory_checks. Binary floats can be inexact relative to decimal arithmetic, so the advisory lists the offending constants and suggests decimal.Decimal or exact SymPy rationals (sympy.Rational) where exactness matters. The advisory is informational only. It is an AdvisoryCheck, which enforces advisory_only=True at construction, so it structurally cannot change the verification status or proof_ref. Expressions with floats still verify normally.

{
  "advisory_checks": [
    {
      "name": "floating-point-constants",
      "advisory_only": true,
      "constraint_id": "precision.float-constants",
      "details": {
        "constants": ["0.1", "0.2"],
        "note": "Binary floating-point values can be inexact; results may differ from exact decimal arithmetic.",
        "suggestion": "Use decimal.Decimal or SymPy exact rationals (sympy.Rational) where exact arithmetic matters."
      }
    }
  ]
}

When the advisory appears:

Input	Advisory
Float constant (`0.1 + 0.2`, `1000 * (1 + 0.05)**2`)	Yes — `details.constants` lists each distinct constant
Scientific notation (`1e9`, `1e3*x`)	Yes
Complex constant (`1.0j`)	Yes — complex literals are binary-float-based
Equation input (`0.1 + 0.2 = 0.3`, `0.5x = 0.5x`)	Yes — both sides are parsed lexically, so float literals are flagged even when symbolic simplification would collapse them
Integers and exact rationals only (`2 + 2`, `1/3`)	No
Unparsable input	No — parse failures are handled by the security gates, not the advisory

The engine checks the expression exactly as you submitted it, before symbolic simplification. Implicit multiplication (0.5x) is normalized for parsing but does not hide the float literal.

Tolerance settings

For floating-point comparisons, you can specify a tolerance:

result = client.verify_math(
    "sqrt(2) = 1.41421",
    tolerance=0.00001  # 5 decimal places
)
# ✓ Verified within tolerance

Tolerance bounding

To prevent inflated tolerances from masking incorrect results, the math engine enforces a deterministic upper bound on the tolerance parameter. QWED computes the maximum allowed tolerance as a function of the result’s magnitude:

max_tolerance = max(0.01, abs(calculated_value) * 0.01)

If the requested tolerance exceeds this bound, QWED rejects the verification with a BLOCKED status instead of returning a potentially misleading VERIFIED result. This applies to both decimal and float precision modes.

# Blocked — tolerance far exceeds the computed bound
result = client.verify_math("1 + 1", expected_value=999, tolerance=1000)
# result["status"] == "BLOCKED"
# result["error"] == "Tolerance exceeds deterministic verification bound"
# result["max_allowed_tolerance"] == "0.02000000"

# Allowed — tolerance is within bound for a large result
result = client.verify_math(
    "10000 * (1 + 5/100)",
    expected_value=10540,
    tolerance=50,
)
# result["status"] == "VERIFIED"

The engine also rejects invalid tolerance values (negative numbers, NaN, Infinity, or non-numeric strings) with a BLOCKED status and an "Invalid tolerance" error message.

Tolerance input	Behavior
Within computed bound	Normal verification proceeds
Exceeds computed bound	`BLOCKED` with `max_allowed_tolerance` in response
Negative, `NaN`, or `Infinity`	`BLOCKED` with `"Invalid tolerance"` error
Non-numeric string	`BLOCKED` with `"Invalid tolerance"` error

Trust boundary

When math verification runs through the natural language pipeline (POST /verify/natural_language), the response includes a trust_boundary object. This object describes exactly what the pipeline proved and what it did not, separating deterministic expression evaluation from the non-deterministic LLM translation step — and records the mandatory attestation admission decision.

{
  "trust_boundary": {
    "query_interpretation_source": "llm_translation",
    "query_semantics_verified": false,
    "verification_scope": "translated_expression_only",
    "deterministic_expression_evaluation": true,
    "formal_proof": false,
    "translation_claim_self_consistent": true,
    "provider_used": "openai",
    "trust_enforced": "VERIFIED",
    "attestation_policy": "mandatory",
    "overall_status": "VERIFIED"
  }
}

Field	Type	Description
`query_interpretation_source`	string	Always `"llm_translation"` — indicates the query was interpreted by an LLM
`query_semantics_verified`	boolean	Always `false` — QWED cannot verify that the LLM correctly interpreted the user’s intent
`verification_scope`	string	Always `"translated_expression_only"` — the attestation `qwed.query_hash` also binds to this translated expression, not the natural-language query
`deterministic_expression_evaluation`	boolean	`true` when the inner engine status was `VERIFIED` or `DISPROVEN`
`formal_proof`	boolean	Always `false` — SymPy evaluation is deterministic but not a formal proof of the original query
`translation_claim_self_consistent`	boolean	Whether the translated expression matched its own claimed answer
`provider_used`	string	The LLM provider used for translation
`trust_enforced`	string	Status returned by the mandatory trust-boundary enforcement step. Always matches `overall_status`.
`attestation_policy`	string	Always `"mandatory"` — the control plane requires a signed attestation before returning a `VERIFIED` result
`attestation_error`	string	Present only if attestation signing failed. Machine-readable code (e.g. `SIGNING_FAILURE`, `CRYPTO_UNAVAILABLE`) that caused the downgrade to `BLOCKED`.
`overall_status`	string	The top-level response status after trust boundary enforcement — always sourced from the enforced decision, never from the raw verifier verdict

Because the LLM translation step is non-deterministic, the natural language pipeline never admits a result: admission is always BLOCKED, even when the translated expression is VERIFIED. The verdict carries verification_scope: "translated_expression_only" and query_semantics_verified: false, so it can’t be mistaken for proof of your question. Use the direct POST /verify/math endpoint if you need a fully deterministic result without the LLM translation layer.

Mandatory attestation admission

The control plane runs every math response through enforce_trust_decision(..., require_attestation=True). Attestation is now an admission gate — a VERIFIED result is only returned once the signing step succeeds:

On success: the verifier evidence (translated expression, calculated value, claimed value, diff, precision mode) is passed to create_verification_attestation(). If the returned AttestationResult has status == ISSUED, enforce_trust_decision accepts the signed token and sets overall_status = "VERIFIED".
On signing failure: the response is downgraded to BLOCKED and trust_boundary.attestation_error records the error code from the AttestationResult (for example SIGNING_FAILURE or CRYPTO_UNAVAILABLE). No token is returned. This is a fail-closed guarantee: signing outages never surface as VERIFIED.
overall_status is post-attestation. It is always sourced from the enforced decision, never from the raw verifier verdict. If you need to reason about the raw verifier output separately, inspect verification.is_correct and deterministic_expression_evaluation.

Attestation scope: translated expression, not natural-language query

The attestation qwed.query_hash binds to the translated expression that the deterministic engine actually evaluated (task.expression), not to the user’s natural-language query. This matches the disclosed verification_scope: "translated_expression_only" and prevents the attestation from over-claiming that the user’s prose was verified.

response.user_query — the original natural-language query, kept for display and audit correlation.
Attestation qwed.query_hash — SHA-256 of the translated deterministic expression (e.g. 0.15 * 200), which is the exact input the engine executed.
Downstream verifiers should hash the translated expression when re-checking qwed.query_hash. Hashing user_query will not match — that is intentional, because QWED does not attest to the LLM translation step.

{
  "user_query": "What is 15% of 200?",
  "translation": {
    "expression": "0.15 * 200",
    "claimed_answer": 30.0
  },
  "trust_boundary": {
    "verification_scope": "translated_expression_only",
    "attestation_policy": "mandatory"
  },
  "attestation": "eyJhbGciOiJFUzI1NiIs..."
  // qwed.query_hash inside the JWT = sha256("0.15 * 200")
}

Ambiguous expressions

Expressions with implicit multiplication after division are ambiguous — for example, 1/2(3+1) could mean (1/2)*(3+1) or 1/(2*(3+1)). Rather than guessing, the math engine fails closed and returns BLOCKED:

result = client.verify_math("1/2(3+1)")
# result["is_valid"] == False
# result["status"] == "BLOCKED"
# result["warning"] == "ambiguous"

To resolve this, rewrite the expression with explicit parentheses or a * operator:

# Explicit grouping — no ambiguity
result = client.verify_math("(1/2)*(3+1)")
# ✓ Verified: 2.0

result = client.verify_math("1/(2*(3+1))")
# ✓ Verified: 0.125

Expression input rules

Every math expression passes through a layered structural validator before SymPy evaluates it. The validator runs in order: NFKC Unicode normalization, an ASCII character-set gate, a construct denylist, and an AST node-type allowlist. An expression that fails any layer is rejected before evaluation. These are the rules your expressions must follow:

Rule	Rejected	Write instead
Decimal points need a digit on both sides	`.5`, `2.`	`0.5`, `2.0`
ASCII characters only	`α + 1`, `２＋２`	`alpha + 1`, `2+2`
No string or bytes literals	`"abc" + x`	Remove the string
No attribute access	`x.real`, `(2).bit_length()`	Not supported
No comparisons, booleans, or assignment	`x > 1`, `True`, `a = b`	Use an equality claim (`lhs = rhs`) at the top level only
No subscripts, brackets, or semicolons	`a[0]`, `{x}`, `1; 2`	Not supported
No lambdas or comprehensions	`lambda: 1`	Not supported

Additional details:

Greek letters: the parser provides ASCII names for the full Greek alphabet (alpha, beta, gamma, … omega). Write alpha * x, not α * x. Non-ASCII codepoints never reach the parser, including Unicode look-alikes that NFKC-normalize to ASCII identifiers.
Allowed characters: letters, digits, underscore, whitespace, and the operator set + - * / ( ) . , ^ %.
Allowed syntax: arithmetic operators, function calls from the safe namespace (sin, cos, log, sqrt, factorial, …), symbol names, and numeric constants. Everything else is rejected by the AST allowlist.
Caret exponentiation: ^ is converted to ** by the default transformation pipeline, so x^2 and 2^3 parse correctly.
Depth and length limits: expressions are capped at 5,000 characters, an AST depth of 30, and a SymPy tree depth of 40.
Implicit multiplication (2x, sin x, 2(x+1)) still parses. These forms are covered by the character-set gate instead of the AST check.

# Rejected — bare decimal
result = client.verify_math(".5 * 200 = 100")
# Validation error: write 0.5

# Rejected — non-ASCII symbol
result = client.verify_math("α^2 + 1 = 2")
# Validation error: use alpha

# Accepted
result = client.verify_math("0.5 * 200 = 100")
# ✓ Verified

result = client.verify_math("(alpha + 1)^2 = alpha^2 + 2*alpha + 1")
# ✓ Verified: algebraic identity

These rules are structural security guarantees, not style preferences. Attribute access, string constants, and non-ASCII identifiers are the building blocks of sandbox-escape payloads, so the parser rejects them by construction rather than pattern-matching known attacks. Legitimate arithmetic never needs them.

Compute-cost bounds

SymPy expands integer powers eagerly and exactly. An expression like 9^9^9^9 demands a result with billions of digits, so evaluating it would hang the engine. The parser now estimates the exact-expansion cost of every expression statically and rejects expressions that exceed the budget before evaluation starts. The bounds are:

Bound	Limit	Rejected example
Integer literal magnitude	`10^300`	A 400-digit literal
Exponent magnitude	`10,000`	`2^100000`
Result digit budget	`100,000` digits	`9^9999^9999` (power tower)
`factorial` / `binomial` argument	`10,000`	`factorial(100000)`

Additional details:

Power towers and caret chains are folded right-associatively and checked as a whole, so ((9^9)^9999)^9999 and 9^9^9^9 are both caught even though each individual exponent is small.
Concrete-valued calls are evaluated statically. Wrapping a large value in abs(), factorial(), binomial(), or a numeric constructor does not hide it from the gate: 2^abs(-100000) and 2^factorial(10000) are both rejected.
All cost comparisons use exact arithmetic, never binary floats, so the estimates are deterministic.

A rejected expression fails validation before evaluation, with an error message naming the exceeded bound:

# Rejected — exponent exceeds the 10,000 magnitude bound
result = client.verify_math("2^100000 = 0")
# Validation error: exponent exceeds the static bound

# Rejected — power-tower expansion exceeds the digit budget
result = client.verify_math("9^9999^9999 = 0")
# Validation error: expansion would exceed the digit budget

# Accepted — well within bounds
result = client.verify_math("2^100 = 1267650600228229401496703205376")
# ✓ Verified

These bounds are far above anything legitimate verification needs — 2^100, factorial(500), and 300-digit results all pass. They only reject expressions whose exact expansion is computationally unbounded.

Edge cases

Scenario	Behavior
Division by zero	Returns error, not verified
Undefined expressions	Returns “UNDEFINED” status
Complex numbers	Fully supported
Very large numbers	Uses arbitrary precision
Symbolic variables	Verified algebraically
Oversized tolerance	Returns “BLOCKED” status with details
Invalid tolerance	Returns “BLOCKED” with error message
Sampling-only identity match	Returns “BLOCKED” — no formal proof established
Ambiguous implicit multiplication	Returns “BLOCKED” — rewrite with explicit operators
Bare decimal (`.5`, `2.`)	Rejected before evaluation — write `0.5`, `2.0`
Non-ASCII characters (`α`, fullwidth digits)	Rejected before evaluation — use ASCII names like `alpha`
Strings, attribute access, comparisons, subscripts	Rejected by the AST allowlist — see Expression input rules
Non-equality expression in batch verification	Returns `is_valid: false` with `status: "SIMPLIFIED"` — simplification is not a proof
Oversized exponent, power tower, or huge factorial	Rejected before evaluation — see Compute-cost bounds
Ambiguous mode (multimodal data)	Returns “BLOCKED” with `ambiguous_modes` — only a unique mode can verify
Incomplete or over-complete eigenvalue claim	Returns “DISPROVEN” with `calculated_count`/`claimed_count`
Identity that only holds after cancelling a removable singularity (`x/x = 1`)	Returns “UNVERIFIABLE” with `constraint_id: math.domain_restricted_identity`
Float rounding residue or non-finite value in a mismatch	Returns “INCONCLUSIVE” (`UNVERIFIABLE`), not disproven
Unit conversion across dimensions (`m` to `kg`)	Returns “BLOCKED”
IRR with multi-root, derivative stall, or non-convergence	Returns “BLOCKED” — no best-effort iterate is returned
Float or complex constants in the expression	Verdict unchanged — a `precision.float-constants` advisory is attached to `advisory_checks`

Performance

Operation	Avg Latency	Throughput
Simple arithmetic	1.5ms	690/sec
Complex expression	5ms	200/sec
Identity proof	10ms	100/sec

Next steps

Logic engine - Verify logical constraints
Code engine - Verify code correctness
API reference - Full API documentation

​Capabilities

​Quick start

​Core operations

​1. Expression evaluation

​2. Identity verification

​Domain-restricted identities

​3. Derivatives

​Derivatives in /verify/math identities

​Parse errors

​4. Integrals

​5. Limits

​Financial calculations

​Compound interest

​Net present value (NPV)

​Internal rate of return (IRR)

​Verdicts and admission

​Fail-closed semantics

​verify_statistics(statistic="mode") — unique mode required

​verify_matrix_operation(operation="eigenvalues") — cardinality match required

​verify_irr — convergence proof

​Trust boundary

​Error handling

​Exact SymPy arithmetic

​Decimal precision

​Float precision advisory

​Tolerance settings

​Tolerance bounding

​Trust boundary

​Mandatory attestation admission

​Attestation scope: translated expression, not natural-language query

​Ambiguous expressions

​Expression input rules

​Compute-cost bounds

​Edge cases

​Performance

​Next steps

Capabilities

Quick start

Core operations

1. Expression evaluation

2. Identity verification

Domain-restricted identities

3. Derivatives

Derivatives in `/verify/math` identities

Parse errors

4. Integrals

5. Limits

Financial calculations

Compound interest

Net present value (NPV)

Internal rate of return (IRR)

Verdicts and admission

Fail-closed semantics

`verify_statistics(statistic="mode")` — unique mode required

`verify_matrix_operation(operation="eigenvalues")` — cardinality match required

`verify_irr` — convergence proof

Trust boundary

Error handling

Exact SymPy arithmetic

Decimal precision

Float precision advisory

Tolerance settings

Tolerance bounding

Trust boundary

Mandatory attestation admission

Attestation scope: translated expression, not natural-language query

Ambiguous expressions

Expression input rules

Compute-cost bounds

Edge cases

Performance

Next steps