feat(symbolic): T6 -- SQLi/race-condition pattern-matching prototype, real RuleEngine bug fix

Fase 5 of the research roadmap: SQL Injection Prevention and No
Check-Then-Act Race have existed as KG rules since the project's
earliest seed data, each with a PRE/POST formal_spec, but neither was
ever wired to anything that extracts those preconditions from real
code -- prompt guidance only, never independently checked.

symbolic/security_facts.py adds two narrow, well-documented AST fact
extractors (SQL query built via concatenation/f-string/%-format/
.format() into an execute-like call, with one-hop variable resolution
and recognition of the safe parameterized-query idiom; unguarded
check-then-act on a shared container, tracking real with-block
containment for the lock guard). Z3 cannot help here regardless --
microsoft/z3guide's own Strings page (fetched as real evidence in the
prior evidence-pipeline work) states its string solver is "an
incomplete heuristic solver" and the combined theory "is not decidable
anyway."

Wiring the race-condition extractor's output into the pre-existing
RuleEngine.apply_rule_to_code surfaced a real design gap, not by
inspection but by running it: that method is a positive-derivation
checker (precondition met -> derive postcondition -> PASS) with no
code path that ever returns FAIL, for any input. Fed a rule whose PRE
names a dangerous pattern, meeting that PRE derives the POST and
reports PASS on genuinely vulnerable code. Fixed via a new, additive
check_for_violation method (apply_rule_to_code itself untouched --
nothing else calls it) with the inverse framing: FAIL if the trigger
is present and unmitigated, PASS if mitigated, UNKNOWN if the trigger
doesn't apply (never an affirmative "proven safe"). Also corrected SQL
Injection Prevention's formal_spec from prose to the same fact-string
syntax No Check-Then-Act Race already happened to use.

Verified end-to-end against hand-written vulnerable/safe fixtures for
both patterns (neither existing security benchmark covers SQLi or race
conditions) and against the two closest existing security-benchmark
shapes, with zero false positives.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

Author: Juanpacol

docs/CASE_STUDY.md

@@ -173,16 +173,62 @@ the cross-day noise floor — meaning the KG-context effect, unlike the
 retry-loop trade-off, is not just noise. Both the retraction and the
 survival came from applying the identical check; neither was assumed.
 
+## Finding 6 — a rule engine that had been sitting there, quietly unable to fail
+
+Two KG rules — `SQL Injection Prevention` and `No Check-Then-Act Race` —
+existed in the seed data since the project's earliest commits, each with
+a `PRE`/`POST` formal spec describing exactly the pattern it should
+catch. Neither had ever been wired to anything that reads real code:
+they were retrieved into the LLM's prompt as guidance and never checked
+independently. Building that check (Fase 5 of the research roadmap, T6)
+meant writing two small AST-based fact extractors and feeding their
+output into `RuleEngine.apply_rule_to_code` — the method that already
+existed for exactly this purpose.
+
+It returned `PASS` on the vulnerable sample. Not a crash, not an
+exception — a clean, confident, wrong answer on code containing the
+exact unguarded check-then-act race the rule's own precondition names.
+
+The cause wasn't the new fact extractors; they were behaving correctly.
+`apply_rule_to_code` is a forward-chaining *derivation* checker (the IBM
+NSTK pattern this module cites in its own module docstring): precondition
+met → derive the postcondition → report `PASS`. That's the right
+behavior for deriving new facts from established ones. It is exactly the
+wrong behavior for "does this code violate a rule," because the method
+has no branch that returns `FAIL` — not a missing case that happens not
+to trigger here, but structurally absent from the function for any
+input. Feed it a rule whose precondition *is* the dangerous pattern, and
+meeting that precondition is treated as license to derive the "safe"
+postcondition and call it done. The second rule didn't even reach that
+bug: its formal spec was prose (`PRE: user_input is untrusted`) rather
+than a fact string, so it silently never fired at all — `UNKNOWN`,
+matching nothing, for a different reason than intended but at least not
+a false `PASS`.
+
+The fix was small and additive on purpose: a new `check_for_violation`
+method with the inverse framing (precondition present + postcondition
+absent → `FAIL`; postcondition present → mitigated `PASS`; precondition
+absent → `UNKNOWN`, never an affirmative "proven safe"), plus correcting
+the SQL rule's formal spec to real fact-string syntax. `apply_rule_to_code`
+itself was left untouched — nothing else in the codebase calls it, so
+there was no reason to risk its behavior for a legitimate forward-chaining
+caller that might exist later. The bug had been shippable-looking code
+for as long as those two rules existed; it just had never been asked a
+question it could get wrong until real facts from real code were run
+through it.
+
 ## The pattern
 
-None of these five findings came from writing more tests against the
+None of these six findings came from writing more tests against the
 existing fakes — they came from running the actual thing (or, in Finding
-5's case, re-checking a real run's own numbers harder) and dealing
-honestly with what happened, including retracting a prior claim, instead
-of defending it. That's the habit this case study is meant to name: a
-comprehensive offline test suite is a floor, not a ceiling. It proves the
-system does what the scripts told it to expect. It cannot prove the
-system does the right thing when something *unscripted* happens — and
-something unscripted is exactly what a real model, a real database, or a
-real user (or a second run of the same experiment) will always eventually
-do.
+5's case, re-checking a real run's own numbers harder, and in Finding 6's,
+finally connecting two pieces that had each looked fine in isolation) and
+dealing honestly with what happened, including retracting a prior claim,
+instead of defending it. That's the habit this case study is meant to
+name: a comprehensive offline test suite is a floor, not a ceiling. It
+proves the system does what the scripts told it to expect. It cannot
+prove the system does the right thing when something *unscripted*
+happens — and something unscripted is exactly what a real model, a real
+database, or a real user (or a second run of the same experiment, or
+finally wiring up a rule that had sat dormant since the beginning) will
+always eventually do.

docs/PHASE_3_METHODOLOGY.md

@@ -501,6 +501,104 @@ CLAUDE.md anticipates may behave differently — this ablation only covers
 10-48 rules, not the order-of-magnitude jump a real production corpus
 would represent.
 
+## T6 — can pattern-matching close the SQLi/race-condition gap? (2026-07-15)
+
+Fase 5 of the research roadmap: `docs/CASE_STUDY.md` and this document
+already note SQL injection and race-condition detection as explicitly out
+of Z3's scope (arbitrary string/heap reasoning isn't something an SMT
+solver decides). The KG seed data
+(`kg/seed_data/security_rules.json`) has carried a `SQL Injection
+Prevention` rule and a `No Check-Then-Act Race` rule since the project's
+earliest seed data was written -- both with `PRE`/`POST` formal specs --
+but neither had ever been wired to anything that extracts those
+preconditions from real code. They were prompt guidance only: injected
+into the LLM's context via retrieval, never independently checked.
+
+**What was built**: `symbolic/security_facts.py`, two narrow AST-based
+fact extractors -- `extract_sql_injection_facts` (flags a query string
+built via concatenation/f-string/%-format/`.format()` and passed to an
+`execute`/`executemany`/`executescript`-named call, one hop through a
+local variable; recognizes the parameterized-query safe idiom) and
+`extract_race_condition_facts` (flags an `if key in container:` /
+`container.get(key)` check followed by a subscript assignment to the same
+container, anywhere in a function, with no enclosing lock-named `with`
+block). Both are deliberately narrow and say so in their own docstrings
+-- e.g. no cross-function data-flow, no ORM query builders, direct
+self-recursion-style syntactic matching only. Z3 genuinely cannot help
+here: the real evidence fetched in the evidence pipeline
+(`docs/evidence/z3_docs/z3_docs_d192712d2ab1.json`, microsoft/z3guide's
+own Strings theory page) states its string solver is "an incomplete
+heuristic solver" and the combined theory "is not decidable anyway" --
+this isn't a workaround for a temporary VerityAI limitation, it's the
+actual state of the art.
+
+**A real design gap found while wiring this up, not by inspection**:
+feeding the vulnerable-race sample's own extracted fact
+(`check_then_act_on_shared_resource`, which IS the KG rule's own PRE
+condition, verbatim) into the pre-existing `RuleEngine.apply_rule_to_code`
+returned `PASS`. Tracing why: that method is a positive-derivation
+checker built for the IBM NSTK forward-chaining pattern ("precondition
+met -> derive postcondition -> report PASS") -- it has no code path that
+returns `FAIL`, for any input, ever. Fed a rule whose PRE names a
+*dangerous* pattern, meeting that PRE derives the POST and reports PASS
+-- an actively misleading verdict on genuinely vulnerable code, not
+merely a missing feature. Separately, the SQL Injection Prevention rule's
+`formal_spec` (`PRE: user_input is untrusted; POST: query uses
+parameterized statement`) was prose, not fact-string syntax, so it didn't
+even reach that bug -- it just silently never fired (`UNKNOWN`,
+precondition text matching nothing).
+
+**Fixed, minimally, in this session**: added `RuleEngine.check_for_violation`
+as a new, additive method (nothing else in the codebase calls
+`apply_rule_to_code`, so its existing behavior for legitimate forward-
+chaining callers was left untouched) with the inverse framing -- PRE is
+the trigger condition, POST is the required mitigating fact: `FAIL` if
+the precondition holds and the postcondition fact is absent, `PASS` if
+the postcondition fact is present (mitigated), `UNKNOWN` if the
+precondition doesn't apply at all. Also corrected the SQL Injection
+Prevention rule's `formal_spec` to real fact-string syntax (`PRE:
+sql_query_built_dynamically; POST: uses_parameterized_query`), matching
+the vocabulary `extract_sql_injection_facts` actually produces --
+`No Check-Then-Act Race`'s spec already happened to be written that way.
+
+**Verified end-to-end against hand-written fixtures** (neither
+`correctness_benchmarks.json` nor `security_benchmarks.json` contains a
+real SQLi or race-condition sample -- confirmed by inspection; the
+existing security tasks are divide-by-zero, bounds-checks, and a
+lock-flag proxy, all Z3-reducible):
+
+| Sample | Extracted facts | `check_for_violation` |
+|---|---|---|
+| Vulnerable SQL (string concat into `execute`) | `sql_query_built_dynamically`, `sql_query_built_via_concatenation` | **FAIL** — violated, unmitigated |
+| Safe SQL (`?` placeholder + params tuple) | `uses_parameterized_query` | UNKNOWN — trigger absent (never a false PASS) |
+| Vulnerable race (unguarded check-then-act) | `check_then_act_on_shared_resource` | **FAIL** — violated, unmitigated |
+| Safe race (same pattern inside `with lock:`) | `check_and_act_combined_atomically` | UNKNOWN — trigger absent |
+
+No false positives on the two existing security-benchmark shapes tested
+(`security_003`'s lock-flag proxy, `security_005`'s bounds-check) --
+neither extractor fires on int-only assertion code, as expected.
+
+**Honest scope of the answer**: pattern-matching genuinely can close part
+of this gap -- for the textbook shape of each vulnerability, with the
+caveats documented in each extractor's own docstring (no cross-function
+tracking, no ORM builders, ~one-hop variable resolution for SQL). It
+cannot certify absence of a vulnerability (`check_for_violation` never
+returns an affirmative "no injection risk exists" -- only "found a
+violation" or "found nothing to check"), and race conditions in
+particular remain much shakier ground than SQL injection: the check-then-
+act shape covers exactly one classic pattern, not the much larger space
+of real concurrency bugs (cross-thread interleavings, async races,
+missing memory barriers). **Recommendation**: worth extending
+`security_facts.py` with a handful more OWASP-shaped extractors
+(path traversal, command injection via string-built shell commands --
+`security_scan.py`'s blocklist already covers the `os.system`/`subprocess`
+call surface, so this would be extending pattern coverage of *arguments*
+to already-flagged calls, not new call surface) before wiring any of this
+into the live orchestrator's retry loop as an actual verification gate;
+today it's a prototype demonstrating the fact-extraction approach works
+and the existing `RuleEngine` had a real, fixable gap, not a
+production-ready scanner.
+
 ## Target threshold (confirmed before a real run, per the plan's hardened
 acceptance criterion)
 

src/verityai/kg/seed_data/security_rules.json

@@ -33,7 +33,7 @@
     "description": "Verify that SQL queries use parameterized queries, not string concatenation",
     "category": "security",
     "severity": "critical",
-    "formal_spec": "PRE: user_input is untrusted; POST: query uses parameterized statement",
+    "formal_spec": "PRE: sql_query_built_dynamically; POST: uses_parameterized_query",
     "applies_to": [
       "python",
       "java",

src/verityai/symbolic/rule_engine.py

@@ -173,6 +173,58 @@ def apply_rule_to_code(
 
         return VerificationStatus.UNKNOWN, f"No consequence derived from {rule.name}"
 
+    def check_for_violation(
+        self, rule: Rule, code_facts: dict[str, Any]
+    ) -> tuple[VerificationStatus, Optional[str]]:
+        """Checks whether `code_facts` indicates a VIOLATION of `rule`, not
+        whether the rule's derivation fires -- the opposite framing from
+        `apply_rule_to_code`.
+
+        `apply_rule_to_code` is a positive-derivation checker: "precondition
+        met -> derive postcondition -> PASS." It can structurally only ever
+        return PASS or UNKNOWN -- there is no code path in it that returns
+        FAIL, for any input. That's correct for the forward-chaining
+        derivation this class was built for (IBM NSTK pattern), but it means
+        it cannot express "this code violates a security rule" at all: fed
+        a rule whose PRE names a *dangerous* pattern (e.g. `No Check-Then-
+        Act Race`'s `PRE: check_then_act_on_shared_resource`), a vulnerable
+        snippet's own extracted facts satisfy that PRE, `apply_rule_to_code`
+        derives the POST and reports PASS -- an inverted, actively
+        misleading verdict on genuinely vulnerable code. Found via T6's
+        real prototype (`symbolic/security_facts.py`), not by inspection.
+
+        This method treats PRE as "the trigger condition to check for" and
+        POST as "the required mitigating fact" instead: FAIL if the
+        precondition holds and the postcondition fact is absent from
+        `code_facts`, PASS if the postcondition fact IS present (the danger
+        was mitigated), UNKNOWN if the precondition doesn't apply here at
+        all. Added as a new method rather than changing
+        `apply_rule_to_code`'s behavior, since nothing else in this
+        codebase calls it and there was no need to risk its existing
+        semantics for callers that legitimately want plain derivation.
+        """
+        if not rule.formal_spec or "PRE:" not in rule.formal_spec:
+            return VerificationStatus.UNKNOWN, f"Rule {rule.name} has no PRE/POST formal_spec"
+
+        fact_strings = set(code_facts.keys())
+        self.reset()
+        self.facts = fact_strings
+
+        if not self._preconditions_met(rule):
+            return VerificationStatus.UNKNOWN, f"Rule {rule.name} precondition not present"
+
+        consequence = self._derive_consequence(rule)
+        if consequence and consequence in self.facts:
+            return (
+                VerificationStatus.PASS,
+                f"Rule {rule.name}: mitigated ('{consequence}' present)",
+            )
+
+        return (
+            VerificationStatus.FAIL,
+            f"Rule {rule.name} violated: precondition present, '{consequence}' not confirmed",
+        )
+
     def get_applicable_rules(
         self, code_facts: dict[str, Any], language: str = "python"
     ) -> list[Rule]: