(feature) Hypothesis & Correctness: a neurosymbolic verification architecture

Abstract

SkillSpector is a security gate — its score decides whether a skill is "safe to install" — but it grew as an imperative tool, so its correctness invariants were never stated, only embedded. This proposal asks how to put that gate on a verified footing. The core idea is neurosymbolic: we can't formally verify the LLM at the center, but we can verify the deterministic safety envelope around it (the rules that keep a real CRITICAL finding from being dropped) by treating the LLM as an arbitrary adversarial oracle. We adapt AWS's Cedar methodology — an authoritative executable model bridged to production code by differential testing in CI — to a code-first, partly-neural Python codebase. The first deliverable is not code but a ratified specification: an archaeology pass that recovers each behavior and has a maintainer rule it intended, incidental, or bug. The full architecture is below; this top section is for a go/no-go decision.

Pitch for maintainers

The problem, concretely. The risk score, the severity bands, and the LLM finding-filter are the load-bearing safety logic, and they're guarded today by example-based tests. Nothing establishes that a real CRITICAL survives the LLM filter for every possible (including prompt-injected) model response, or that the score behaves sanely across all inputs. For a tool whose whole job is to be trusted, that gap is the product.

This isn't theoretical — the archaeology already surfaced two issues. While reading the scoring code we found (1) score depends on the input order of equal-severity findings, so adding a low-confidence finding can lower the score (report.py:111-135), and (2) the 0-100→[0,1] confidence rule is inconsistent across call sites (>1.0 vs a historical >2.0). Both are exactly the kind of latent defect that a stated, checked specification would have caught — and that example tests didn't.

Why the approach is credible, not academic. It copies a methodology AWS already ships in production (Cedar): a small executable model as the source of truth, kept honest against the real code by differential random testing in CI. We adapt it to reality here — Python reference model first (no new toolchain, survives the OSS-sync merges), heavyweight proofs (Lean/Dafny) held in reserve for the one deep theorem that actually needs them (the adversarial-oracle envelope). We also draw an honest line: the LLM itself is out of formal scope; we verify the symbolic guardrails, not the model.

Why it's good open-source work. It's self-contained (lives in tests/ + a spec module, touches no production behavior), naturally tiered for contributors of different levels (property tests → reference model + DRT → optional theorem proving), and produces durable artifacts — a readable spec and a CI gate — that outlast any one contributor. It's also a strong showcase: "continuous formal verification of an AI-security tool" is a recruiting and credibility win for the project.

The decision we're asking for. Is this worth pursuing, and at what ceiling? Three forks gate everything (see §7): (1) fidelity — universal proof of the envelope, or exhaustive-where-finite + adversarial sampling elsewhere? (2) substrate — start with a Python reference model (recommended), or evaluate Lean/Dafny up front? (3) home — downstream verification overlay, or upstream contribution with a real release gate? A "yes, at fidelity X" unblocks the no-tooling archaeology pass as step one.

Status: Architecture / design proposal. No source or test changes are made by this document. It (a) frames how verified development applies to a code-first, partly-neural tool, (b) records the raw archaeology material, and (c) surfaces the architectural decisions that must be made before any verification code is written.

Origin: docs/tasks/0001-hypothesis-correctness.md. Prompted by commit 47c75223511f8ead154954c03293cc981ad4e569 (PR #32, "isolate Stage 2 batch failures and keep unanalysed findings").

Architectural inspiration: AWS, "Lean into verified software development" (the Cedar methodology) — see §4.

1. Problem & framing

SkillSpector is a security gate: its output decides whether a skill is "safe to install." Correctness failures are asymmetric — a dropped/under-scored CRITICAL is dangerous (false negative); noise is merely annoying (false positive). The system is tuned to fail toward false positives (fail-closed). The question this document addresses is whether we can establish that those safety properties hold, continuously, rather than hoping the example-based tests happen to cover them.

1.1 SkillSpector is already neurosymbolic

The pipeline mixes two kinds of computation, and they have different verifiability:

The neural layer reads attacker-controlled skill text, so the LLM is not merely non-deterministic — it is potentially adversarial. You cannot verify the LLM. You can verify the deterministic safety envelope that wraps it, by modeling the LLM as an arbitrary oracle and proving the envelope holds for all of its outputs. That is the neurosymbolic answer, and it determines the whole architecture below.

2. The inversion: this is code → spec, not spec → code

The single most important fact about applying verified development here:

AWS does verification-guided development: write the model, prove theorems, then write the code. SkillSpector is the reverse — the code already exists, grew imperatively, and the invariants were never stated up front. Some are recorded in DEVELOPMENT.md as an afterthought; most are emergent.

This inversion changes what the first deliverable is. When the model comes first (AWS), every line is intended by construction. When you reconstruct a model from organically-grown code, the code conflates three things that look identical:

1. Load-bearing invariants someone meant (the severity floor; fail-closed — these even carry comments).
2. Incidental-but-fine behavior (the exact 1.3× executable multiplier — a tuning knob, not a law).
3. Incidental-and-wrong behavior nobody decided (see SC-2 in §6 — score depends on the input order of equal-severity findings; it just fell out of a sort key).

2.1 Archaeology is adjudication, not extraction

You cannot mechanically "extract the invariants" from imperative code, because the code is equally happy to exhibit (1), (2), and (3). The recovered behaviors are only candidates. Turning a candidate into a spec line requires a human ruling: intended / incidental / suspected-bug. That ratification step has no shortcut, and it is the archaeology.

Worked example (why this can't be automated). The scoring sort key (report.py:111-114) is (rule_id, severity_rank) with no confidence tie-break. Python's stable sort then orders equal-severity findings by input position, and the diminishing weights (1.0, 0.5, 0.25) are handed out by position. So a low-confidence CRITICAL that appears before a high-confidence one steals the full-weight slot:

• input [conf 0.01, conf 1.0] → 50·1.0·0.01 + 50·0.5·1.0 = 25.5
• input [conf 1.0, conf 0.01] → 50·1.0·1.0 + 50·0.5·0.01 = 50.25

Same findings, different score. The code has no opinion on whether this is correct. Only a human can rule "score must be permutation-invariant → add confidence to the sort key" vs. "input order is meaningful → document it." A hand-written formal model would almost certainly model the sort as severity-descending and prove the bug away — which is exactly why the ratification must precede, and drive, the model.

(SC-2 is asserted from reading report.py:111-135; confirm empirically before filing. It is used here as a methodology example, not yet a ruled defect.)

3. The verification boundary map

Cedar is small and pure, so AWS models all of it. SkillSpector is not uniform — naming the boundary is half the architectural work. Three strata, three obligations:

Key consequences:

• S1 is shallow. score ∈ [0,100] is trivially true by the final min(100, max(0, …)) clamp; band-partition is a complete proof by enumerating range(0, 101). No solver required. Differential testing against a reference model
  • enumeration covers S1.
• S2 is the only genuinely deep, universally-quantified theorem in the system ("for all oracle outputs, every CRITICAL/HIGH input survives"). This is what Hypothesis can only sample and a prover can actually close. If anything here justifies a Lean-grade tool, it is S2 and only S2.
• S3 must be drawn explicitly so a green CI is never mistaken for "the LLM is correct." The boundary map itself is an archaeology deliverable.

4. Target architecture (AWS-shaped, substrate-light)

The transferable skeleton from the Cedar methodology — independent of language:

authoritative executable model ⇄ (differential testing) ⇄ production code, gated at release.

AWS specifics, for reference: an executable Lean model doubles as spec and documentation ("10X smaller than its corresponding Rust implementation"); differential random testing runs "millions of random inputs … both model and code produce the same output," nightly; and "a new version … isn't released unless its model, proofs, and differential tests are up to date."

4.1 What we adopt, and what we change

• Adopt the shape: a separate, authoritative model; DRT as the bridge; a release/merge gate.
• Change the substrate — do not lead with Lean. Start with an executable Python reference model of the S1 cores: a deliberately simple, obviously-correct reimplementation, separate from the evolved production functions, that serves as spec-as-documentation and as the DRT oracle. It needs no second toolchain, no learning curve (AWS's own advice: "start simple"), survives OSS syncs in-language, and gives the shallow S1 strata everything they need.
• Reserve Lean/Dafny for the S2 envelope theorem only. That universal "for-all-oracles" guarantee is the one place a prover earns a second language. Treat it as a separately-justified phase, not the price of entry.

4.2 Continuous verification (the "CI" part)

make verify runs the fast tier; the deep tier runs in scheduled CI. The reference model is the living, readable spec referenced from DEVELOPMENT.md.

5. The OSS-sync constraint (a force AWS doesn't have)

The git history shows periodic Sync OSS release snapshot merges. AWS's release gate only bites when verification ships with the artifact. So there is a prior decision:

• (a) Downstream research overlay — verification lives strictly in tests/ + a standalone spec module, never touching production files, engineered to survive upstream merges. The "gate" is advisory on this fork.
• (b) Upstream contribution — spec + DRT become part of the project and the release gate can actually block. Requires upstream buy-in.

This choice constrains where every artifact below lives, so it is settled first.

6. Raw archaeology material (candidate behaviors — NOT yet ratified)

Recovered from reading the code. Each row is a candidate awaiting the §2.1 adjudication (intended / incidental / suspected-bug). S# = stratum. This is input to archaeology, not the spec.

Scoring & banding — nodes/report.py:89-148 (S1)

LLM-filter envelope — nodes/meta_analyzer.py (S2)

Confidence / batch isolation / dedup / suppression (S1, + S2 for BI-3)

7. Open architectural decisions (settle before writing verification code)

1. Fidelity ceiling. Are we aiming for the universal guarantee on the S2 envelope (the theorem that pulls in a prover), or is "exhaustive-where-finite + DRT / adversarial-sampling everywhere else" the honest target for a tool with an unverifiable LLM at its core?
2. Substrate. Accept "Python reference model now, Lean reserved for the S2 theorem," or evaluate Lean/Dafny up front as the modeling language?
3. Home (per §5). Downstream overlay or upstream contribution? Determines whether a real release gate is on the table.

8. Recommended sequencing

1. Archaeology pass (no tooling). Walk §6 with a maintainer; produce the ratified spec: each behavior tagged intended / incidental / bug, plus the §3 boundary map finalized. File SC-2 and CN-2 as defects-or-decisions. This is the deliverable that must exist before anything else.
2. Decide the three forks in §7.
3. Stand up the S1 reference model + DRT as the CI spine (make verify + nightly), plus exhaustive enumeration for the finite properties (BD-1, SC-1).
4. Adversarial-oracle property testing of the S2 envelope (LF-1..LF-4 over all oracle outputs).
5. (Conditional on §7.1/7.2) Lean/Dafny proof of the S2 envelope theorem, with the reference model as its executable counterpart and DRT as the bridge to production.

My current lean: do step 1 first with no machinery, adopt the AWS shape with a Python reference-model substrate as the spine (steps 3–4), and treat the Lean envelope theorem (step 5) as a separately-justified bet rather than the foundation — but decisions §7 genuinely move this, so they come before commitment.

Appendix — verified scoring formula (read from report.py:89-148)

sort findings by (rule_id, severity_rank asc: CRITICAL<HIGH<MEDIUM<LOW)   # no confidence tie-break → SC-2
score = 0.0
for f in sorted:
    confidence = clamp(f.confidence, 0.0, 1.0)
    if confidence <= 0.0: continue            # SC-6
    base = SEVERITY_POINTS.get(f.severity.upper(), 5)   # 50/25/10/5  (SC-4)
    count = occurrences[rule_id]; occurrences[rule_id] += 1
    if count >= 3: continue                    # SC-5
    weight = (1.0, 0.5, 0.25)[count]           # SC-5  (allocated by position → SC-2)
    score += base * weight * confidence        # SC-3
if has_executable_scripts: score *= 1.3        # SC-8
final = min(100, max(0, int(score)))           # SC-1
band  = first b in [(81,CRIT),(51,HIGH),(21,MED),(0,LOW)] with final >= threshold   # BD-1
rec   = {LOW:SAFE, MEDIUM:CAUTION, HIGH:DO_NOT_INSTALL, CRITICAL:DO_NOT_INSTALL}[band]   # BD-3