> ## Documentation Index
> Fetch the complete documentation index at: https://docs.qwedai.com/llms.txt
> Use this file to discover all available pages before exploring further.
# Math engine
> QWED's Math Engine uses SymPy for symbolic verification of arithmetic, algebra, calculus, trigonometry, financial calculations, and statistics.
The Math Engine is QWED's core verification engine. It uses [SymPy](https://www.sympy.org/) 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
```python theme={null}
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:
```python theme={null}
# 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:
```python theme={null}
# 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")
# ✗ Not Verified: Missing 2ab term
# 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.
### 3. Derivatives
Verify calculus derivatives:
```python theme={null}
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
```
### 4. Integrals
Verify indefinite and definite integrals:
```python theme={null}
# 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
```python theme={null}
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
```python theme={null}
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)
```python theme={null}
result = client.verify_npv(
rate=0.10,
cash_flows=[-1000, 300, 400, 500, 600],
expected=388.07
)
# ✓ Verified
```
### Internal rate of return (IRR)
```python theme={null}
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](#verify_irr-—-convergence-proof) for the full state table.
***
## 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 `CORRECTION_NEEDED` 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 | `CORRECTION_NEEDED` | `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 |
```python theme={null}
# 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](/engines/stats#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 within `1e-6` | `VERIFIED` | Full agreement |
| `len(claimed) == len(calculated)` and any value differs | `CORRECTION_NEEDED` | Values compared pairwise after sorting |
| `len(claimed) != len(calculated)` (under- or over-complete) | `CORRECTION_NEEDED` | `calculated_count` and `claimed_count` returned |
Response fields on the cardinality-mismatch case:
| Field | Type | Description |
| ------------------------ | ------- | ------------------------------------------------------------------------------------------------- |
| `status` | string | `"CORRECTION_NEEDED"` |
| `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` |
```python theme={null}
# CORRECTION_NEEDED — claim omits the second eigenvalue
result = client.verify_matrix_operation(
operation="eigenvalues",
matrix=[[2, 0], [0, 3]],
expected=[2],
)
# result["status"] == "CORRECTION_NEEDED"
# result["calculated_count"] == 2
# result["claimed_count"] == 1
# result["calculated_eigenvalues"] == [2.0, 3.0]
# CORRECTION_NEEDED — repeated root must be listed twice
result = client.verify_matrix_operation(
operation="eigenvalues",
matrix=[[2, 0], [0, 2]],
expected=[2],
)
# result["status"] == "CORRECTION_NEEDED"
# 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` | `CORRECTION_NEEDED` | `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"`, `"CORRECTION_NEEDED"`, 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 |
```python theme={null}
# 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 `CORRECTION_NEEDED`. Treat both statuses as unverified 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 response includes a `trust_boundary` object. This object describes exactly what the pipeline proved and what it did not.
```json theme={null}
{
"status": "INCONCLUSIVE",
"final_answer": 30.0,
"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": "INCONCLUSIVE"
}
}
```
| 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 |
The overall status for natural language math queries is `INCONCLUSIVE` because, while QWED evaluates the expression deterministically, it cannot verify that the LLM correctly interpreted the user's intent. The `trust_boundary` gives you the information to decide whether the result is sufficient for your use case.
***
## Error handling
When verification fails, QWED provides detailed error information:
```python theme={null}
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:
```python theme={null}
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`](/advanced/diagnostics), which enforces `advisory_only=True` at construction, so it structurally cannot change the verification `status` or `proof_ref`. Expressions with floats still verify normally.
```json theme={null}
{
"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:
```python theme={null}
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.
```python theme={null}
# 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.
```json theme={null}
{
"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": "INCONCLUSIVE",
"attestation_policy": "mandatory",
"overall_status": "INCONCLUSIVE"
}
}
```
| 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 `CORRECTION_NEEDED` |
| `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 returns `INCONCLUSIVE` instead of `VERIFIED` even when the underlying expression evaluation succeeds. This prevents over-representing a translated-query evaluation as a proven user-query verdict. 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`](/advanced/attestations#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.
```json theme={null}
{
"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`:
```python theme={null}
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:
```python theme={null}
# 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.
```python theme={null}
# 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:
```python theme={null}
# 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](#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](#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 "CORRECTION\_NEEDED" with `calculated_count`/`claimed_count` |
| 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](./logic) - Verify logical constraints
* [Code engine](./code) - Verify code correctness
* [API reference](/api/endpoints) - Full API documentation