Parent: #7. Lane: Agent-E. Depends on agent-ix/quire-specification#124, agent-ix/quire-contract-ir#136 V1-E09 and agent-ix/quire-spec-language#198 V1-A15 (abstraction relation). Woven in after V1-E09 (agent-ix/quire-contract-ir#136) and after #101 closeout; no priority change.
Primary capabilities: Verus emission onto implementation Rust (2026-09-18 proof-backend amendment; V1-BACK-020 minted by quire-specification#124).
Normative contracts: the Verus-emission FR added by quire-specification#124; FR-036; AD-010.
Emit Verus requires/ensures and loop invariants from QSL state contracts onto named implementation Rust functions, through the abstraction relation exported by QSL V1-A15 (agent-ix/quire-spec-language#198). The template is the Kani function-contract wrapper in src/kani.rs (subject_path, kani::requires/kani::ensures); the Verus path reuses its subject addressing and adds the relation-based state mapping. A claim whose model elements have no bound relation refuses, per V1-BACK-022.
Solver needed: Verus. Absence path: warned unsupported when Verus is not installed; a result Verus reports proved records trust basis solver-asserted.
Exit: one ConfigVersion operation verifies under Verus against its QSL contract; a mutated implementation fails; an unbound model element refuses; Kani emission unchanged.
Parent: #7. Lane: Agent-E. Depends on agent-ix/quire-specification#124, agent-ix/quire-contract-ir#136 V1-E09 and agent-ix/quire-spec-language#198 V1-A15 (abstraction relation). Woven in after V1-E09 (agent-ix/quire-contract-ir#136) and after #101 closeout; no priority change.
Primary capabilities: Verus emission onto implementation Rust (2026-09-18 proof-backend amendment; V1-BACK-020 minted by quire-specification#124).
Normative contracts: the Verus-emission FR added by quire-specification#124; FR-036; AD-010.
Emit Verus
requires/ensuresand loop invariants from QSL state contracts onto named implementation Rust functions, through the abstraction relation exported by QSL V1-A15 (agent-ix/quire-spec-language#198). The template is the Kani function-contract wrapper insrc/kani.rs(subject_path,kani::requires/kani::ensures); the Verus path reuses its subject addressing and adds the relation-based state mapping. A claim whose model elements have no bound relation refuses, per V1-BACK-022.Solver needed: Verus. Absence path: warned
unsupportedwhen Verus is not installed; a result Verus reports proved records trust basissolver-asserted.Exit: one ConfigVersion operation verifies under Verus against its QSL contract; a mutated implementation fails; an unbound model element refuses; Kani emission unchanged.