Math engine

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")
# ✗ 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:

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:

# 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.

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

# 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 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`

# 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

# 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.

{
  "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:

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": "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 (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 “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 - Verify logical constraints
Code engine - Verify code correctness
API reference - Full API documentation

Overview

Core Engines

Analysis Engines

Specialized Engines

Capabilities

Quick start

Core operations

1. Expression evaluation

2. Identity verification

3. Derivatives

4. Integrals

5. Limits

Financial calculations

Compound interest

Net present value (NPV)

Internal rate of return (IRR)

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

​3. Derivatives

​4. Integrals

​5. Limits

​Financial calculations

​Compound interest

​Net present value (NPV)

​Internal rate of return (IRR)

​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

3. Derivatives

4. Integrals

5. Limits

Financial calculations

Compound interest

Net present value (NPV)

Internal rate of return (IRR)

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