Update from code changes: 3-tier engine classification - #244
Update from code changes: 3-tier engine classification#244mintlify[bot] wants to merge 2 commits into
Conversation
|
Skipping PR review because a bot author is detected. If you want to trigger CodeAnt AI, comment |
QWED Security Verification Report2 files scanned | 0 blocked | 0 warnings | 0 info | 0 suppressed | 2 verified Engines
Verified Files
Verified by QWED — deterministic security verification. No LLM used. |
|
You are seeing this message because GitHub Code Scanning has recently been set up for this repository, or this pull request contains the workflow file for the Code Scanning tool. What Enabling Code Scanning Means:
For more information about GitHub Code Scanning, check out the documentation. |
|
Preview deployment for your docs. Learn more about Mintlify Previews.
|
|
Preview deployment for your docs. Learn more about Mintlify Previews.
|
Greptile SummaryReframes verification documentation around three output-guarantee tiers.
Confidence Score: 2/5The PR should not merge until its response examples and automatic guard-routing claims match the documented SDK and DiagnosticResult contracts. The changed overview teaches invalid status values and response shapes while also implying that generic verification invokes security guards which require explicit calls, creating concrete integration and enforcement failures. Files Needing Attention: engines/overview.mdx and architecture.mdx
|
| Filename | Overview |
|---|---|
| engines/overview.mdx | Introduces the tier model, but its response examples conflict with DiagnosticResult, its automatic guard-routing claims conflict with the documented SDK, and Taint is classified inconsistently. |
| architecture.mdx | Narrows deterministic claims and links the tier model, but retains a lifecycle status vocabulary inconsistent with DiagnosticResult. |
Flowchart
%%{init: {'theme': 'neutral'}}%%
flowchart TB
P[Proof engines<br/>Evidence] --> E[Policy enforcement<br/>Decision]
E --> A[Advisory engines<br/>Analysis]
Reviews (1): Last reviewed commit: "docs: sharpen SEO titles and description..." | Re-trigger Greptile
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
| ```python | ||
| # Example: fact verification is deterministic | ||
| result = client.verify_fact( | ||
| claim="Paris is in France", | ||
| context="Paris is the capital of France." | ||
| ) | ||
| # Uses TF-IDF similarity + entity matching | ||
| # No LLM needed for most claims | ||
| { | ||
| "status": "BLOCK", | ||
| "engine": "ConfigGuard", | ||
| "reason": "SECRETS_DETECTED", | ||
| "decision_trace": ["match:OPENAI_API_KEY@api_key"] | ||
| } |
There was a problem hiding this comment.
When integrators copy these policy and advisory examples, BLOCK and ADVISORY do not match the linked DiagnosticStatus values, and the advisory data is placed outside developer_fields; this causes rejected results, unmatched status branches, or lost advisory checks.
Context Used: AGENTS.md (source)
| class A advisory; | ||
| ``` | ||
|
|
||
| A single verification request flows through the tiers: proof engines attempt a deterministic proof, policy enforcement engines apply runtime rules, and advisory engines contribute structured diagnostics. Only the proof tier can produce a `VERIFIED` status. |
There was a problem hiding this comment.
When users pass retrieval contexts or MCP tool definitions to generic client.verify, this documented tier flow implies that RAGGuard or MCPPoisonGuard runs automatically, but the SDK requires explicit guard calls; relying on this flow leaves those inputs unchecked.
Context Used: AGENTS.md (source)
| | Engine | Backend | Domain | | ||
| |---|---|---| | ||
| | [Math](/engines/math) | SymPy + Decimal | Arithmetic, calculus, matrices, NPV/IRR | | ||
| | [Logic](/engines/logic) | Z3 | SAT/SMT, quantifiers, BitVectors | | ||
| | [SQL](/engines/sql) | SQLGlot AST | Query structure, complexity, schema | | ||
| | [Code](/engines/code) | Multi-language AST | Python, JS, Java, Go security analysis | | ||
| | [Schema](/engines/schema) | Pydantic + Math | JSON structure + embedded calculations | | ||
| | [Stats](/engines/stats) | Pandera + Wasm | Data-frame invariants, sandboxed exec | | ||
| | Symbolic | CrossHair | Reference `DiagnosticResult` engine | |
There was a problem hiding this comment.
The primary proof-engine table omits Taint even though the documentation index below places it under Proof engines and the architecture page groups it with structural and data-flow proofs. Add it to this table or reclassify the other references so readers can determine which output guarantee applies.
Context Used: AGENTS.md (source)
Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!
1 participant
Summary
Reframes the verification engines overview around the three formal engine tiers — Proof, Policy Enforcement, and Advisory — and cross-references the classification from the architecture page.
Changes
engines/overview.mdx:architecture.mdx: constrain the deterministic-verification claim to supported proof domains and link to the new engine classification.Context
Follows QWED-AI/qwed-verification#247, which formalizes the target
DiagnosticResultengine classification: only proof engines emitVERIFIED+proof_ref; policy enforcement engines emitBLOCK/UNVERIFIABLE; advisory engines emitAdvisoryCheckonly and can never emitVERIFIED.