Research: independent formal cross-check and Rust-level soundness verification (Rocq / Verus / Aeneas / Isabelle) #451

Classification

• Type: bounded research / proof-obligation feasibility (not a production feature)
• Priority: P3 / backlog, not on the critical path
• Area: production Roslyn → OwnIR → Rust own-analysis ownership transfer/join → diagnostic assumptions
• External prior art: Astrée: abstract interpretation and absence-of-error claims; Isabelle/HOL and its Programming and Proving tutorial
• Related, not replaced: Research: IKOS-inspired abstract-state soundness oracle and operator audit (bounded spike) #433 (IKOS-inspired independent concrete oracle/operator mutation), Research: map domain-theoretic fixed-point assumptions to Own.NET's ownership analysis #450 (domain/fixpoint assumption mapping), Research: FORVES2-style conditional semantic validation and proof-assumption audit for OwnIR #445 (FORVES2-style conditional equivalence and trusted premises), Research: SootUp-inspired OwnIR/ICFG semantic-fidelity and incomplete-call audit (bounded spike) #430 (Roslyn→OwnIR fidelity), Research: evaluate Bifrost for C# code intelligence, agent navigation, and evidence contracts #426 (completeness/evidence), P-037 kernel: solve_with / lfp_chaotic returns Some(non-fixpoint) on an unfair schedule #368 (P-037 fairness counterexample), PR #367 (existing Rocq/MathComp proof and Rust-table/certificate seam for the separate P-037 kernel).

Motivation

Astrée's transferable lesson is the explicit link between a concrete semantics, a conservative abstraction, and the scope of the claimed absence of errors, not its C/C++ numerical domains or commercial implementation. Isabelle/HOL is one possible way to machine-check a small theorem about that link.

Own.NET already has lattices/dataflow and a formal P-037 experiment. In PR #367, Rocq/MathComp proves results for the isolated P-037 kernel and checks a Rust truth-table seam. Do not mistake those results for a proof that the main Rust ownership analyzer, its C# lowering, or production diagnostics are sound.

The uncovered question is narrow:

For one existing production ownership operation, can we formulate and (if practical) machine-check a non-vacuous soundness obligation against a small, independently justified concrete resource model, with an auditable connection to the actual implementation?

This is not a request to introduce Isabelle for its own sake. Reuse/extend the existing Rocq proof infrastructure by default if a proof assistant is warranted; compare Isabelle/HOL only when a specific advantage can be demonstrated.

Preflight / no-duplication gate

1. Pin the current Own.NET revision and inspect actual Rust state/transfer/join code, OwnIR contract, relevant C# lowering, the P-037 formal notes and PR research: MathComp applicability spike for Own.NET #367 artifacts. Do not infer features (widening, narrowing, aliases, exceptional edges) that the selected implementation does not actually model.
2. Read Research: IKOS-inspired abstract-state soundness oracle and operator audit (bounded spike) #433, Research: map domain-theoretic fixed-point assumptions to Own.NET's ownership analysis #450 and Research: FORVES2-style conditional semantic validation and proof-assumption audit for OwnIR #445 first. If the precise theorem/semantics and implementation seam are already covered, close as DUPLICATE / ALREADY-COVERED with links. Do not build a second concrete-state oracle, mutation harness, general domain-theory essay or conditional equivalence checker.
3. Identify a single proof seam outside the already-proved P-037 kernel, preferably an actual resource-state transfer or branch join in the production Rust ownership analysis. Record why it matters to a known risk or evidence claim.

Bounded work

A. State the semantics and proof contract

Specify a tiny independently reviewable concrete resource machine, only for the selected operation, with explicit limitations (e.g. resource identity, aliasing, ownership, acquire/use/release, modeled control-flow edges). Define:

• C: concrete states and transition step_C;
• A: the existing abstract states and transfer/join step_A;
• R(c, a) / concretization γ(a): what it means for an abstract state to cover a concrete state;
• an explicit unknown/unmodeled boundary, including unresolved calls or exceptional behavior if the chosen seam cannot represent them.

Candidate obligation (adapt to the actual semantics):

R(c, a) ∧ step_C(c, op) = c'
    ⇒ R(c', step_A(a, op))

For nondeterministic/exceptional transitions, quantify over every modeled concrete successor. For a join, prove each incoming state's concretization is included in the join's concretization. Never translate omitted successors, timeouts, unsupported constructs, or an incomplete frontier into a proof of safety.

Keep distinct: (1) transfer over-approximation, (2) completeness of source→OwnIR lowering, (3) solver termination/fixpoint assumptions, and (4) end-user diagnostic correctness. Proving (1) does not prove (2)–(4).

B. Evaluate a proof approach, kill-first

• Baseline: inspect whether the existing Rocq/MathComp code, P-037 exporter/certificate pattern, Kani or small executable exhaustive tests already discharge the selected obligation.
• Try one minimal machine-checked theorem only if there is a justified new obligation. Prefer reusing Rocq; assess Isabelle/HOL as an alternative, not an additional mandatory dependency. Note comparative encoding effort, automation, assumptions and executable-implementation linkage.
• If formalization invents a parallel toy semantics with no checkable connection to Own.NET's selected production operator, STOP rather than claiming a soundness result.
• If feasible, use a small test-only comparison to pin a finite operator truth table or a clearly defined extraction/certificate boundary. This is a regression/evidence seam, not a general proof that compiled Rust implements a specification.

C. Negative controls and audit

• Try at least one deliberately wrong transfer/join rule (e.g. dropping a feasible alias/path) and show that the theorem fails or a counterexample is produced; if not possible, document why.
• State all assumptions and trusted components, including any admitted/axiomatized facts, finite bounds, model exclusions and the source→OwnIR gap.
• Explain what result would actually change an Own.NET decision, as opposed to merely adding a proof artifact.

Deliverables / acceptance criteria

• A concise, pinned overlap map vs Research: IKOS-inspired abstract-state soundness oracle and operator audit (bounded spike) #433/Research: map domain-theoretic fixed-point assumptions to Own.NET's ownership analysis #450/Research: FORVES2-style conditional semantic validation and proof-assumption audit for OwnIR #445, P-037/PR research: MathComp applicability spike for Own.NET #367, with a distinct selected proof seam or early STOP.
• One concrete/abstract semantics and proof-obligation note (including R/γ, modeled successors and unmodeled cases) tied to named production functions/types at a pinned revision.
• Rocq reuse vs Isabelle/HOL comparison with evidence; no default new prover/toolchain or mandatory CI dependency.
• If justified, one reproducible machine-checked property, its exact assumptions, and a negative control; otherwise a well-supported NO-GO. Do not imply that finite enumeration is a general proof.
• Separate verdicts for model theorem, Rust implementation correspondence, Roslyn/OwnIR semantic fidelity, solver completeness, and diagnostic guarantee; each marked PROVED / TESTED / ASSUMED / UNMODELED / UNKNOWN.
• Final decision: DUPLICATE / STOP / RESEARCH-ONLY / NARROW FOLLOW-UP, with reproduction commands, cost and a concrete benefit/gap.

Non-goals

No full C# semantics, whole-program soundness claim, wholesale Astrée port, numerical abstract domains, new production solver, speculative diagnostic suppression or production SAFE upgrades. Do not re-prove the already-covered P-037 kernel or duplicate #433's property/mutation corpus. Any production change requires a separate, independently justified issue.

References

• Astrée research project
• Isabelle/HOL / documentation
• Own.NET #433, #450, #445, #368, PR #367

Addendum (2026-10-30): independent cross-formalization and production Rust verification

Why expand #451? The original ticket deliberately selected one production ownership transfer/join soundness obligation. Keep that target, definitions, baseline controls, negative controls, deliverables and research-only boundaries intact. The additional question is whether independent specifications and a direct implementation-facing verifier can reveal defects that an internally consistent Rocq model, Kani harness or operator tests miss. A second green proof is not automatically additional confidence.

This addendum supersedes only the earlier tool-selection preference (“Isabelle as an alternative, not an additional dependency” and “prefer Rocq”): independent Isabelle/HOL is now an explicitly admissible complementary experiment if it has a distinct error-detection hypothesis. The original one selected production seam, no-default-dependency, cost/STOP and evidence-boundary constraints remain.

What was already done / ownership map (do not duplicate)

Three distinct verification lanes (evaluate, do not adopt all by default)

Lane A — proof against executable Rust (Verus; compare Kani baseline first).

• Pin one existing own-analysis resource-state operator and identify its actual types and callers.
• Test whether Verus supports the selected Rust fragment without rewriting the operator into a second implementation. Its spec/proof/exec split and optional dual_spec / exec_spec_verified! approaches deserve investigation, but do not assume those cover arbitrary existing Rust or generics.
• Express e.g. γ(a) ∪ γ(b) ⊆ γ(join(a,b)) or preservation of every modeled concrete successor; verify an implementation-facing postcondition where possible. A wrapper that simply assumes the desired postcondition or reimplements the algorithm does not count.
• Keep Kani's bounded results as a separate comparator. Kani PASS is not an unbounded proof; Verus PASS is only for its supported code/contracts and trusted solver/semantic assumptions.
• If the pinned function cannot be verified without invasive refactoring or trusted external-body stubs, report UNSUPPORTED/NO-GO.

Lane B — source-to-proof translation (Charon + Aeneas → Lean, optionally Rocq/HOL4).

• On the same pinned function if feasible, attempt a read-only/test-only Rust→LLBC→pure-model translation. Check exact upstream version, supported subset and external-library models. Aeneas does not provide an Isabelle backend.
• Compare generated behavior against an independently written resource-state requirement, not a theorem copied from the translated implementation. If proof needs invented stubs, list them as trusted assumptions.
• Classify translation success separately from proof success and independently test Rust↔generated-model correspondence on small executable inputs; a successful translation alone is not a proof of semantic preservation or of C# behavior.
• If extraction requires rewriting away relevant effects or silently assuming missing semantics, STOP, even if Lean/Rocq can prove the simplified model.

Lane C — independent semantic adversary (Isabelle/HOL, or another demonstrably independent notation).

• Independently derive a tiny concrete resource model from C# ownership requirements and reviewed examples, not by transcribing Rocq definitions line by line.
• Select different semantic formulations and falsifiable properties (alias/resource identity, may-vs-must, branch join, unknown call effects). Nitpick/Quickcheck can search finite countermodels; Sledgehammer may assist proof construction. A bounded countermodel is a finding candidate, not automatically an executable C# bug.
• Compare findings through the same canonical transition alphabet/test cases with the existing Rocq and Rust evidence. Explicitly inspect whether the two proofs share the same incorrect premise or source model.
• If an Isabelle model merely duplicates Rocq and detects no independent faults, classify DUPLICATE/NO-INCREMENTAL-VALUE; do not maintain two proof stacks for aesthetics.

Cross-checking rationale: Anthropic's Fermat proof artifact used the Lean kernel plus the independent Rust kernel nanoda, with a separate theorem/axiom comparison. That is independent kernel checking of one proof, not two independent models of the program. Both strategies can be useful, but this issue specifically targets independent semantics and implementation correspondence. Anthropic's 2026 formal-verification write-up also describes complementary Verus proof and empirical differential testing; the latter remains testing, not proof.

Concrete pre-registered pilot and negative controls

Gate 0: before installing a tool, record baseline SHA, engine, the actual selected Rust functions, source/OwnIR facts and exact prior coverage; choose one operation with an adjudicated semantic risk (candidate: path join dropping a reachable ownership state, or conditional release incorrectly promoted from may to must). Document why this is not already discharged by #433 or the P-037 proof. If no distinct seam, STOP.

Pilot: at most one selected operator and one closely related boundary; begin with #433's existing independent oracle and Kani fixtures. Try a Verus proof or Aeneas extraction first according to actual Rust-feature support; add independent Isabelle when there is a genuinely different falsification hypothesis. No requirement that all three lanes succeed.

Pre-register a small set of mutants/controls, reusing existing tests rather than inventing a second corpus:

1. Unsound join loses one incoming feasible state.
2. Alias/identity confusion causes release/use/ownership effect on the wrong resource.
3. Conditional may becomes must or unmodeled/opaque call becomes harmless no effect.
4. An explicitly UNKNOWN/INCOMPLETE boundary is accidentally promoted to SAFE.
5. A safe near-neighbor / semantics-preserving control stays accepted, avoiding an always-failing pseudo-check.

Use only applicable mutants and state exclusions honestly. For each, capture which lane found the issue, the first divergence, reproducible input, actual C#/Rust behavior where replayable, specific theorem or countermodel, proof assumptions and tool/build versions. Record whether it is new relative to baseline Rocq/Kani/oracle tests, not merely rediscovery.

Acceptance and decision matrix (additional to, not replacement for, original #451 criteria)

• A tool/semantic-fit table: Rocq baseline / Kani / Verus / Aeneas+Lean (or Rocq) / Isabelle, including exact source-to-proof linkage, assumptions/trusted components, unsupported Rust features, cost, and what independent defect class each can catch.
• For every claimed theorem: prove the intended statement under independently justified premises; list Admitted/axioms, model exclusions, externally supplied functions and how a proof remains linked to selected production Rust. Explicitly separate model proof, translator correctness, implementation correspondence, source→OwnIR fidelity, fixpoint completion and end-user verdict.
• At least one deliberately wrong applicable rule is rejected with a useful witness or failed proof by the new lane, with comparison to existing checks; otherwise report NO-INCREMENTAL-VALUE/UNSUPPORTED, not a nominal PASS.
• For any counterexample, independent concrete replay/adjudication distinguishes REAL-DEFECT, MODEL-ONLY, SPEC-MISMATCH, TRANSLATION-GAP, UNMODELED and INFRA-ERROR. No blanket soundness claim based on synthetic mutants.
• Record exact commits, tool versions, commands, runtime/setup cost, unsupported cases, and a final GO-NARROW / RESEARCH-ONLY / STOP / DUPLICATE disposition. Any real defect gets a separate narrowly scoped bug issue; any production integration gets separate authorization.
• Preserve original Research: independent formal cross-check and Rust-level soundness verification (Rocq / Verus / Aeneas / Isabelle) #451 obligations, completion taxonomy, negative controls and P3/research-only classification. No mandatory new CI dependencies, whole-program Rust/C# proof project, adoption of three provers, new static-analysis engine, or production diagnostic behavior change.

Pinned upstream entry points (to verify again at experiment time)

• Verus source / spec, proof and exec modes / Rust feature support
• Aeneas source / Aeneas documentation
• Isabelle/HOL and its Nitpick/Quickcheck/Sledgehammer documentation
• Anthropic Fermat verification artifact / formal software verification research