Skip to main content

Core Concepts

Understand the philosophy behind QWED.

The Trust Model​

QWED is built on a fundamental insight:

LLMs are probabilistic translators, not reasoning engines.

β”Œβ”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”
β”‚ QWED TRUST MODEL β”‚
β”œβ”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€
β”‚ β”‚
β”‚ β”Œβ”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β” β”Œβ”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β” β”Œβ”€β”€β”€β”€β”€β”€β”€β”€β”€β” β”‚
β”‚ β”‚ USER β”‚ β”‚ LLM β”‚ β”‚ QWED β”‚ β”‚
β”‚ β”‚ (Trusted) │───────▢│ (Untrusted) │───────▢│(Trusted)β”‚ β”‚
β”‚ β””β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”˜ β””β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”˜ β””β”€β”€β”€β”€β”€β”€β”€β”€β”€β”˜ β”‚
β”‚ β”‚ β”‚ β”‚ β”‚
β”‚ Query Probabilistic Verified β”‚
β”‚ Output Result β”‚
β”‚ β”‚
β””β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”˜

How Translation Works​

This is the key to understanding QWED. Let's walk through a real example:

Example: Verifying a Mathematical Claim​

User asks: "Is it true that the sum of interior angles in a triangle equals 180 degrees?"

β”Œβ”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”
β”‚ STEP 1: Natural Language Query β”‚
β”‚ ────────────────────────────────────────────────────────────────── β”‚
β”‚ "Is it true that the sum of interior angles in a triangle β”‚
β”‚ equals 180 degrees?" β”‚
β””β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”˜
β”‚
β–Ό
β”Œβ”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”
β”‚ STEP 2: LLM Translation (Untrusted) β”‚
β”‚ ────────────────────────────────────────────────────────────────── β”‚
β”‚ LLM converts to QWED-Logic DSL: β”‚
β”‚ β”‚
β”‚ (EQ (PLUS angle_a angle_b angle_c) 180) β”‚
β”‚ β”‚
β”‚ ⚠️ This translation MIGHT be wrong - LLM is not trusted! β”‚
β””β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”˜
β”‚
β–Ό
β”Œβ”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”
β”‚ STEP 3: QWED Verification (Deterministic) β”‚
β”‚ ────────────────────────────────────────────────────────────────── β”‚
β”‚ Z3 Solver: Given angle_a + angle_b + angle_c = 180 β”‚
β”‚ Is this satisfiable? β†’ YES (SAT) β”‚
β”‚ Model: {angle_a: 60, angle_b: 60, angle_c: 60} β”‚
β”‚ β”‚
β”‚ βœ… Mathematically proven. Deterministic. Repeatable. β”‚
β””β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”˜
β”‚
β–Ό
β”Œβ”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”
β”‚ STEP 4: Response β”‚
β”‚ ────────────────────────────────────────────────────────────────── β”‚
β”‚ { β”‚
β”‚ "verified": true, β”‚
β”‚ "status": "SAT", β”‚
β”‚ "model": {"angle_a": 60, "angle_b": 60, "angle_c": 60}, β”‚
β”‚ "proof": "Sum of angles = 60 + 60 + 60 = 180 βœ“" β”‚
β”‚ } β”‚
β””β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”€β”˜

Translation Examples​

Natural LanguageQWED-Logic DSLEngine
"x is greater than 5"(GT x 5)Z3
"Is 2+2 equal to 5?"(EQ (PLUS 2 2) 5)SymPy
"x squared plus y squared = 25"(EQ (PLUS (POW x 2) (POW y 2)) 25)Z3
"If raining, take umbrella"(IMPLIES raining umbrella)Z3

Key Principles​

1. Determinism over Probability​

QWED uses symbolic engines (Z3, SymPy) that provide mathematical guarantees:

EngineTechnologyGuarantee
MathSymPyAlgebraic correctness
LogicZ3SAT/UNSAT proof
CodeASTPattern matching
SQLParserSyntax validity

2. Verification, Not Generation​

QWED doesn't generate answersβ€”it verifies them:

# ❌ Wrong approach (generation)
answer = llm.ask("What is 2+2?") # Might hallucinate

# βœ… QWED approach (verification)
answer = llm.ask("What is 2+2?")
verified = qwed.verify(answer) # Deterministic check

3. Transparent Proofs​

Every verification produces a verifiable proof:

result = client.verify("x^2 - 1 = (x-1)(x+1)")
print(result.proof)
# {
# "type": "algebraic_identity",
# "steps": [...],
# "hash": "sha256:abc123..."
# }

Verification Statuses​

StatusMeaning
VERIFIEDClaim is correct, proof generated
FAILEDClaim is incorrect
CORRECTEDClaim was wrong, correction provided
BLOCKEDSecurity violation detected
ERRORVerification engine failed

Attestations​

QWED can produce cryptographic attestations (signed JWTs) that prove a verification occurred:

result = client.verify("2+2=4", include_attestation=True)
print(result.attestation)
# eyJhbGciOiJFUzI1NiIs...

Attestations can be:

  • Embedded in documents
  • Stored on blockchain
  • Verified by third parties

Agent Verification​

For AI agents, QWED provides pre-execution verification:

# Agent wants to execute SQL
decision = agent_service.verify_action({
"type": "execute_sql",
"query": "DELETE FROM users"
})

if decision == "APPROVED":
execute(query)
elif decision == "DENIED":
abort("Dangerous query blocked")

Next Steps​