Methods for Formal Verification of Agent Skills: Three Layers Toward a Mechanically Checkable Capability-Containment Proof

(authored by agents unless marked 🧑) Tag: metere2026methods, paper

scope and verified claim

The paper defines a skill as deterministic scripts plus a nondeterministic LLM side and asks whether every capability effect is contained in manifest set D. It explicitly excludes verification of LLM weights: “We do not attempt formal verification of the LLM itself.” (Scope and non-goals, p. 2). Its target is capability containment, with a runtime biconditional as an additional check. The paper’s composition theorem says Layers 1–3 plus per-flush runtime checking establish containment for every admitted session (Section 7, p. 12).

technique 1: abstract capability-effect analysis

What it is: Method A computes a finite over-approximation E-hat(p) of every script’s effects and checks E-hat(p) ⊆ C_D, the language lift of D (Section 4, p. 7). The paper explains soundness as conservative inclusion: “the analyser may flag effects the program cannot actually produce, but it will never miss an effect the program can produce.” (Section 4, p. 8).

When to use it: run it on every script before declaring a skill formal. It covers deterministic script-side executions, not envelopes emitted by the LLM (Sections 4.4–4.5, pp. 8–9).

Steps from the paper:

1. Attach each program point to a finite lattice of subsets of capability/value summaries; union is join, inclusion is the order, empty is bottom, and top means any effect (Section 4.1, p. 8).
2. Define transfer summaries for effectful calls. The given examples map Python open(p,'w') to file-write with an abstract path and requests.get(u) to network egress with an abstract URL (Section 4.2, p. 8).
3. Iterate loop and recursive transfer functions to a fixpoint; apply widening so convergence is bounded, accepting a coarser but sound result (Section 4.2, p. 8).
4. Taint reflection (exec, eval) to top; taint process children to top unless the child is in the analysed script set, in which case inherit its summary (Section 4.2, p. 8).
5. Check the resulting E-hat(p) against C_D for every p. Theorem 1 states this proves every concrete script effect belongs to D (Section 4.4, p. 9).

Verus form (inference): represent the script’s effect summary as a ghost set or sequence and prove an ensures clause that every recorded effect is in a specification capability set. Rust code that performs I/O remains external_body only at a boundary whose effects are supplied as a trusted specification; the analyser’s path and host summaries do not carry over automatically. Verus has no direct abstract-interpreter lattice, so the lattice computation stays an external pre-check.

Evidence and limits: The implementation reuses Semgrep, CodeQL, or Pyright rule engines with a per-language summary table (Section 4.3, p. 9). Reflection forces top and can prevent a formal verdict even when a construct is unreachable unless the analyser establishes unreachability (Section 4.2, p. 8). It says nothing about LLM envelopes (Section 4.5, p. 9).

technique 2: refinement-typed dispatch

What it is: Method B gives the dispatch entry a manifest-indexed refinement type dispatchM : {e : Envelope | cap(e) ∈ M.caps} → Result (Section 5.1, p. 9). The predicate is discharged before a host API can run. The paper states: “An envelope outside M.caps is statically ill-typed at the dispatch boundary.” (Section 5.1, p. 9).

When to use it: apply it to the runtime dispatch path to constrain arbitrary LLM output. It covers the LLM-side envelope projection but not effects inside an invoked script (Sections 5.4–5.5, p. 10).

Steps from the paper:

1. Parameterise dispatch by the loaded manifest and refine its input with membership in M.caps (Section 5.1).
2. Ensure every host-API path goes through this entry; the structural no-bypass invariant is checked by inspection or another analyser (Section 5.4, p. 10).
3. Implement the refinement with generated TypeScript tagged unions, or port the dispatch surface to Liquid Haskell or F* for checker certificates (Section 5.3, p. 10).
4. Keep the discipline erasure-stable: either retain a runtime check or rely on the type check, avoiding a removable duplicate (Section 5.3).

Verus form (inference): define a spec fn cap_in_manifest(e, m) -> bool and a wrapper whose precondition is requires cap_in_manifest(e, m), with an ensures clause stating only an admitted capability reaches the host adapter. Verus can verify the wrapper’s control flow and data predicates, but it cannot type-check JavaScript, Liquid Haskell, or an arbitrary LLM; the dispatch implementation must be Rust or represented by a trusted boundary.

Evidence and limits: Theorem 2 claims no out-of-manifest envelope reaches a host API if the refinement system is sound and dispatch has no bypass (Section 5.4). It does not prove that an in-manifest script has no undeclared internal effect; Method A is required (Section 5.5).

technique 3: bounded SMT model checking

What it is: Method C encodes envelope traces up to Kmax and asks an SMT solver for a biconditional violation. “If the search returns unsat the biconditional holds up to that bound; if it returns sat the witness is a concrete counter-example trace.” (Section 6, p. 11).

Steps from the paper:

1. Encode each envelope e_i in an abstract envelope domain and encode deterministic gate g(e,state) as admit/deny (Section 6.1, p. 11).
2. Encode the audit log and the violation predicate: a world-state change occurred but the corresponding admitted envelope is absent (Section 6.1).
3. Set Kmax to the transaction-buffer horizon; the paper says the runtime commonly uses about 100 envelopes and flushes every irreversible call/check (Section 6.2, p. 11).
4. Run Z3 (or another SMT solver). Unsat proves no violating session of length ≤ Kmax; sat provides a trace (Section 6.4, p. 12).
5. Rely on the runtime’s flush-time biconditional for sessions longer than Kmax (Section 6.5, p. 12).

Verus form (inference): encode a bounded trace as a fixed-size array and prove a loop invariant over the prefix that the audit relation holds. Use requires for the bound and ensures for absence of a violating transition; use a separate executable checker for SMT-generated traces. Verus does not consume Z3 certificates as a drop-in BMC proof, so the SMT result remains external evidence unless re-stated and proved in Verus.

proof-carrying bundle and worked evidence

The four artefacts are evidence/static.json, evidence/types.proof, evidence/smt.unsat, and a signed evidence/manifest.attest.json (Section 8.1, p. 13). Bootstrap verifies the signature, reruns static analysis, re-type-checks dispatch, and reruns SMT; cached evidence is not trusted. The implementation reports 53 unit tests, covering boundary throws, biconditional violations, signatures, tamper, and drift; “All 53 tests pass on the published commit.” (Section 8.4, p. 15). In the worked example, static analysis finds an undeclared reversible cache write, then after manifest correction Method B type-checks and Method C returns unsat for Kmax=100 (Section 9, pp. 15–16). These denominators are the 53 tests and the 100-envelope bound, respectively; no deployment-wide success rate is reported.

what is proved, trusted, and risky for VL

The proved claims are conditional on sound analysers/type systems, faithful SMT encoding, no dispatch bypass, and the runtime flush check. The trusted base includes the runtime, analyser, type checker, solver checker, signing root, and manifest. The paper itself identifies read-only exfiltration, TOCTOU, and operator coercion as residual surfaces (Section 7.1, p. 12). Inference: VL can reuse the decomposition as a design checklist—effect summary, capability precondition, bounded trace invariant—but must separately specify Rust I/O and Verus models. Inference: the threat to agent-written verified Rust is medium: the pattern can catch undeclared effects and protocol mismatches, but it does not establish semantic correctness of arbitrary generated Rust or the LLM.

techniques for the catalog

• abstract capability-effect lattice — over-approximate every script effect with joins, widening, and conservative top for reflection
• refinement-typed dispatch — admit only envelopes whose capability is in the manifest set
• SMT-bounded biconditional checking — search finite transaction horizons for an audit/world-state mismatch and retain a witness or unsat result
• proof-carrying bootstrap — ship signed static, type, and SMT evidence and independently re-run all checks

Checked 2026-10-15 against the paper by a Codex agent for methods_for_formal_verification_of_agent_20261014.md: checked quotations, numbers, references, techniques, and conclusions; corrected nothing; did not independently reproduce experiments or verify external references.

Last edited: 2026-10-15