Research: AI-assisted ownership-analysis setup with auditable assumptions (TrustInSoft / Microsoft) #452

Classification

• Type: bounded research / AI-assisted analysis setup with reviewable assumptions and independent evidence; P3 research backlog.
• Not: a new analyzer, an automatic repair bot, a soundness proof, or a change to production diagnostic semantics.
• Area: source-level C# resource examples / known call effects → test-only fixtures and explicit assumptions → existing Roslyn/OwnIR/Rust analysis and independent adjudication.
• Related ownership of work: #433 already owns the independent concrete resource-state oracle/operator mutation; #451 owns the machine-checked transfer/join proof; #425 owns method-effect contract tests; #430 owns source→OwnIR fidelity; #426 owns evidence/completeness semantics; #440 owns candidate fix ranking.
• This issue asks a different question: can AI reduce the manual preparation and audit cost of independently judged ownership-test cases and analysis context, without silently introducing false assumptions? No parallel oracle, mutation engine, semantic model, provenance schema or new code-fix workflow.

Motivation / prior art (verified source claims, not adoption claims)

TrustInSoft Analyzer, April 2026 describes AI-generated analysis drivers and stubs for C/C++/Rust workflows, identified in the UI/reports. Its guarantee is tied to the analyzed program and assumptions; generated stubs are not self-validating.

Microsoft, 26 Oct 2026 describes expert-approved knowledge bases for agentic code transformations, validation with independent tests, and the danger of agent-inferred specifications simply preserving pre-existing bugs.

Microsoft SymCrypt / Aeneas / Lean is relevant as an example of a separately checked proof chain for Rust code; the Rust ownership/Aeneas extraction technique does not transfer directly to arbitrary Roslyn/C# or prove Own.NET soundness.

For Own.NET, a TrustInSoft-style C runtime stub/driver is not automatically the right abstraction: the current seam is C# source/Roslyn → OwnIR, call/effect assumptions, resource identities and diagnostics. Do not inject fake implementations into target code or report a restricted harness as whole-program safety.

Question and hypotheses

Can a constrained agent, given a reviewed ownership contract and an existing fixture, propose:

1. minimal test-only C# variants / call-effect assumption candidates;
2. explicit assumption → source/contract evidence → independently adjudicated expectation records;
3. a reproducible test setup with known modeled/unmodeled boundaries;

...and reduce analyst time or uncover a concrete missing path, without laundering generated assumptions into SAFE?

Bounded experiment

Gate 0: overlap / pinned baseline

1. Inspect Research: OpenTaint-style contract tests and engine-gap triage for method-effect models #425/Research: evaluate Bifrost for C# code intelligence, agent navigation, and evidence contracts #426/Research: SootUp-inspired OwnIR/ICFG semantic-fidelity and incomplete-call audit (bounded spike) #430/Research: IKOS-inspired abstract-state soundness oracle and operator audit (bounded spike) #433/Research: independent formal cross-check and Rust-level soundness verification (Rocq / Verus / Aeneas / Isabelle) #451 and the actual revision of the production Rust ownership core. If they already provide an identical workflow, DUPLICATE / STOP.
2. Select 4–6 preregistered small known-positive/known-negative C# ownership cases (conditional Dispose; alias identity; consuming vs borrowed call; unresolved/opaque call; normal/exceptional exit only where modeled). Pin source, expected outcome, runtime/toolchain versions and available existing harness.
3. Write human-reviewed ground truth and assumptions before any model proposals. Held-out adversarial examples may not be shown to the generation agent.

A/B comparison

• A / baseline: engineer prepares the existing fixture + trace/effect assumptions with current tooling.
• B / assisted: AI proposes only test-only fixtures, possible call-effect summaries and an assumption ledger; engineer reviews each semantic claim before it becomes an input. Reuse Research: OpenTaint-style contract tests and engine-gap triage for method-effect models #425/Research: IKOS-inspired abstract-state soundness oracle and operator audit (bounded spike) #433 oracles for checking, never the generated fixture itself as its own oracle.
• Run the same actual analyzer on both; report independently adjudicated TP/FN/FP/inconclusive and first divergence where available.
• Record review minutes, iterations, discarded suggestions, false assumptions, missing facts, supported/unmodeled cases and setup burden. Small sample is case-study evidence, not population-wide accuracy.

Required adversarial controls

• The generated call summary treats an unknown/virtual method as pure/no-op.
• An alias to an already-disposed object is silently treated as an independent live resource.
• A fixture excludes the exceptional/early-return cleanup edge that actually changes the outcome.
• A driver silently strengthens a precondition to hide a real counterexample.

A correct process rejects or visibly marks such assumptions as UNJUSTIFIED/UNMODELED/INCONCLUSIVE, not SAFE. Include a deliberately clean control to catch alarm inflation.

Provenance / review boundary (reuse existing contracts)

For each candidate fixture/assumption: source SHA, selected method and scope, claim and origin, human review, supported semantics, excluded paths, expected/observed result, analyzer mode, raw evidence reference, and completion/unknown state. First inventory whether existing evidence artifacts can express this; no second result schema by default.

Acceptance / kill criteria

• One table mapping overlap and exact non-overlap versus Research: OpenTaint-style contract tests and engine-gap triage for method-effect models #425/Research: evaluate Bifrost for C# code intelligence, agent navigation, and evidence contracts #426/Research: SootUp-inspired OwnIR/ICFG semantic-fidelity and incomplete-call audit (bounded spike) #430/Research: IKOS-inspired abstract-state soundness oracle and operator audit (bounded spike) #433/Research: independent formal cross-check and Rust-level soundness verification (Rocq / Verus / Aeneas / Isabelle) #451; STOP when the added question is not distinct.
• 4–6 fixed, pre-reviewed cases, or documented inability to set up a fair comparison.
• Matched A/B results including all failed proposals, at least 2 applicable adversarial assumption-injection controls and a clean witness.
• Separate SUPPORTED / REJECTED-ASSUMPTION / UNMODELED / INCOMPLETE / INFRA-ERROR statuses; never infer whole-analyzer soundness from passing fixtures.
• Measured incremental setup/review cost and a specific new defect or evidence improvement; otherwise NO-GO.
• Final GO-NARROW / RESEARCH-ONLY / NO-GO / DUPLICATE with reproducible commands, pinned versions and honest boundaries.

Explicit non-goals: no production LLM dependency, source rewrite, inference-time online services, new framework/solver, generated stubs trusted automatically, always-on CI agent, broad rewrite of C# ownership semantics, or unconditional SAFE classifications. This issue only records and scopes a research experiment; any production integration requires separate approval.