Research: requirements-to-code conformance checking (BDD + reviewed formal contracts + OwnIR evidence) #448

Classification

• Type: bounded research / product-discovery + feasibility spike
• Priority: P3 / research backlog, not a production feature request
• Working name: Requirements-to-Code Conformance Checker ("BDD plus proof-oriented checks")
• Area: natural-language requirements → reviewed machine-checkable contracts → C# code/event mapping → static/runtime verification → source-level counterexamples → PR/CI traceability
• Related Own.NET: Research: FeaVer/Ultimate-style property-guided model extraction and source-level witnesses (bounded spike) #447 (FeaVer/Ultimate model extraction and witnesses; underlying technical spike), Research: evaluate BAIT Büchi inclusion and antichain fixpoints for temporal ownership protocols (bounded spike) #446 (BAIT/Büchi inclusion; separate temporal research), P1: Add Obligation Protocols for project-specific barrier-sensitive rules #272 (obligations), P2: Extend MOS/effect summaries to protocol and barrier effects #274 (protocol/effect summaries), feat(progress): Own.Progress — detect consume-or-exit loop stalls (PRG001) #275 (loop progress), Canonical first-party call facts: preserve interprocedural calls instead of collapsing them into frontend release/use/escape guesses #382 (canonical call facts), Research: IKOS-inspired abstract-state soundness oracle and operator audit (bounded spike) #433 (soundness oracle), Research: Tai-e-inspired semantic fact assertions and selective precision (bounded spike) #443 (semantic-fact assertions)
• Relevant prior art: NASA FRET (constrained language → formal properties), FeaVer (code-to-model/property verification), Microsoft Coyote (systematic C# concurrency testing), Reqnroll (BDD examples/step definitions). These tools solve parts of the pipeline; none alone proves arbitrary natural-language text matches arbitrary C# code.

Hypothesis

Teams already document desired behavior in issue descriptions, acceptance criteria, business rules, ADRs, and sometimes regulatory documents, but a passing BDD scenario or unit test covers only the selected examples.

Could Own.NET help check generalizable, explicitly approved properties against an implementation, and flag previously unanticipated executable paths or version/state combinations?

Desired product-level outcome:

Given requirement R (with source/version), an approved formal interpretation P, and code revision C, report VIOLATED with a reproducible source-linked witness, PROVEN only within an explicitly declared complete model, or UNKNOWN / NOT COVERED when the system cannot justify either.

The natural-language → property step is not trusted. LLM output is a candidate for human review, never an independent proof that the requirement was interpreted correctly.

Motivating example (illustrative; not a request to embed customs semantics in Own.NET)

Human description: "A declaration may be submitted only after validation succeeds."

Ambiguities to surface before analysis:

• Must validation apply to the same version of the declaration that is submitted?
• Does editing fields invalidate prior validation?
• What counts as a blocking error vs warning?
• Are there explicit, source-backed exceptions?

Candidate reviewed property:

Submit(d, version=v) ⇒ a successful Validate(d, version=v) happened since the last relevant mutation and no blocking errors remain

A branch that bypasses validation, or a mutation between validation and submit, may violate this property. The verifier must map events to real C# calls/effects and object identity/version; simply checking that Validate() is somewhere earlier in the method is inadequate.

What makes this different from BDD

• BDD/Reqnroll: curated executable examples through step definitions. Very useful, but does not exhaust unenumerated paths.
• Property-based testing: many generated inputs under a test oracle; strong testing, not a proof of all behaviors.
• Own.NET-backed static verification: explores represented branches/states/transfers within the declared model, returning a valid source witness or stating limits.
• Runtime/systematic testing (optional): can validate a candidate counterexample or explore scheduling-dependent paths; explicitly label tested vs proved.

Do not market one green BDD suite, a bounded search, or an incomplete call graph as a universal conformance proof.

Gate 0: inventory and product constraints

1. Review Research: FeaVer/Ultimate-style property-guided model extraction and source-level witnesses (bounded spike) #447 and the existing Roslyn→OwnIR→CFG/MOS/obligations/progress pipeline. Identify reusable event facts, call resolution, source locations, analysis completion status, and diagnostic codeFlows.
2. Check existing required/available BDD and property-based testing paths in the repo. Do not introduce Reqnroll, FRET, LTL, Promela, SMT, or a new DSL simply because prior-art tools exist.
3. Define a traceability record: requirement ID + original text/span/URL + source document version/effective date + approved interpretation/reviewer + property schema version + mapped code symbols/commit + verifier result/coverage limits. Do not assert current legal correctness from an outdated or unverified regulation.
4. Determine whether this is better developed as an external opt-in layer/product consuming Own.NET evidence, rather than widening ownership diagnostics by default.

Gate 1: choose a narrow property language and baseline

Start with a small, auditable set of business/protocol patterns:

• Never / forbidden-before: operation B forbidden while an obligation is open or before event A.
• Only-after / version-matched: B requires a successful A for the same identified entity/version with no intervening invalidation.
• Must-close-before-exit: obligation opened must be discharged before return/throw (when modeled).
• Conditional permission: operation permitted only if a specified predicate has been established; unknown predicate ≠ false/true.

Avoid arbitrary prose, unrestricted first-order logic, temporal liveness, distributed-system correctness and whole-program equivalence in the first vertical.

For each candidate:

• Pin the original requirement, reviewer-approved expected semantics, and one or more relevant code entry points.
• Map business verbs to actual operations/effects with manual correction and source citations.
• Specify unknown policy for opaque calls, reflection, dynamic code, external services, state persistence, async/concurrency, missed mutation/alias edges, and missing data.
• Compare a cheap baseline first: handwritten assertions/BDD and existing Own.NET rules; ensure the idea offers distinct marginal value beyond P1: Add Obligation Protocols for project-specific barrier-sensitive rules #272/P2: Extend MOS/effect summaries to protocol and barrier effects #274/Research: FeaVer/Ultimate-style property-guided model extraction and source-level witnesses (bounded spike) #447.

Gate 2: bounded pilot, not product rollout

Use 10 real, permission-appropriate requirements from a single C# domain with 2–3 implementable property shapes. Freeze the acceptance oracle before looking at tool output. Prepare independently reviewed fixtures per requirement:

• correct implementation,
• seeded/real violating implementation (including a branch bypass),
• near-neighbor negative to test false positives,
• one UNKNOWN case with deliberately unresolved call/effect or incomplete model.

At least one case should involve validation → mutation/version change → use, to defeat naive "check A was called sometime" heuristics, provided the required identity/version facts exist; otherwise mark it as a verified representational blocker.

Optional system shape:

human requirement + provenance
         ↓
LLM candidate property + ambiguities
         ↓
human-reviewed property / scope / assumptions
         ↓
mapped source operations + OwnIR facts
         ↓
existing checker / small test-only monitor
         ↓
VIOLATED + path | PROVEN (scoped) | UNKNOWN + reason
         ↓
requirement↔code↔commit evidence for PR/CI

Evaluate two distinct questions:

1. Specification fidelity: how often did LLM propose the correct meaning, miss a condition, invent a constraint, or require clarification? Do not silently repair meaning after seeing model output.
2. Implementation analysis: with an approved fixed property, how often were real violations found, false alarms raised, and unknowns honestly reported? Keep errors in spec translation separate from errors in code analysis.

Baselines: existing BDD/unit tests and current Own.NET rules, using the same reviewed corpus. Report number of new confirmed violations not already caught by those baselines, not just raw findings.

Success / STOP criteria

• Short state-of-the-art / donor map (FRET vs FeaVer vs Reqnroll/Coyote vs existing Own.NET).
• Concrete traceability record and a human-approval step for every property.
• Frozen corpus: 10 reviewed requirements, corresponding implementation/control fixtures, and explicit assumptions.
• Distinct spec-translation outcomes and code-verification outcomes (TP/FP/FN/UNKNOWN, by case and reason); no invented accuracy percentage.
• At least one adjudicated new violation missed by the existing baseline, or compelling quantified reduction in review/diagnostic effort; otherwise STOP-NO-INCREMENTAL-VALUE.
• A sample report linking requirement text/version → approved property → relevant C# symbols → source-level witness → code commit, with clear coverage/completeness limits.
• Decide GO-EXTERNAL-PILOT, DEFER-MISSING-FACTS, or STOP-NO-UTILITY; any production changes become separately scoped issues, with owner approval and Python/Rust parity requirements where applicable.

Hard guardrails

• No autonomous legal interpretation: regulation references are inputs with revision, effective date, jurisdiction and human approval, not proof of legal compliance.
• No universal "code implements issue" claim from an LLM, incomplete CFG, missing calls, bounded execution or unsound abstraction.
• Never convert UNKNOWN / INCOMPLETE to PASS or use an unverified candidate witness as an executable bug claim.
• No production code/OwnIR schema or language overhaul, no default CI blocking, and no user-authored Gherkin/Promela requirement.
• Do not duplicate Research: FeaVer/Ultimate-style property-guided model extraction and source-level witnesses (bounded spike) #447 (mechanics of model extraction), Research: evaluate BAIT Büchi inclusion and antichain fixpoints for temporal ownership protocols (bounded spike) #446 (Büchi inclusion), or P1: Add Obligation Protocols for project-specific barrier-sensitive rules #272/P2: Extend MOS/effect summaries to protocol and barrier effects #274/feat(progress): Own.Progress — detect consume-or-exit loop stalls (PRG001) #275 (specific existing analyzers).