From d9452fef8aa78378ee69ab328fd837fd41a81295 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 15 Jul 2026 22:53:57 +0200 Subject: [PATCH] fix(proof-synthesis): correct two miscited claims (claim-verification sweep) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Verified every external citation in the skill against the actual sources (WebFetch of each arXiv page). Findings: - arXiv 2605.26457 (Verus-SpecGym, '26% LLM-as-judge miss'): CORRECT — a prior honesty pass wrongly flagged it as future-dated/unconfirmed; the paper is real (May 2026, Parno/Welleck et al.) and states the figure verbatim. No change. - arXiv 2409.13082 (AutoVerus, 90%/150 tasks): CORRECT. - arXiv 2511.17330 (AutoRocq): CORRECT. - miniF2F '100%': CORRECT (Seed-Prover 100% valid / 99.6% test, 2507.23726). Two fixes: - arXiv 2511.11829 was MISCITED for the Lean row — it is about NL-requirement autoformalization, not Lean-4 spec-equivalence proving. Re-pointed to CLEVER (2505.13938), which actually does prove Lean spec-equivalence. - Softened the CLEVER claim: 'no SOTA agent verifies more than 1 / spec-equivalence the dominant wall' is not supported by the source's abstract; reworded to the supported 'struggle to achieve full verification; the spec is the first-class hard task.' Version: skill 0.4.0 -> 0.4.1; plugin 0.14.0 -> 0.14.1. Co-Authored-By: Claude Opus 4.8 (1M context) --- .../pulseengine-claude/.claude-plugin/plugin.json | 2 +- .../pulseengine-claude/skills/proof-synthesis/SKILL.md | 9 +++++---- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/claude-tooling/plugins/pulseengine-claude/.claude-plugin/plugin.json b/claude-tooling/plugins/pulseengine-claude/.claude-plugin/plugin.json index 65a92ca..4f86061 100644 --- a/claude-tooling/plugins/pulseengine-claude/.claude-plugin/plugin.json +++ b/claude-tooling/plugins/pulseengine-claude/.claude-plugin/plugin.json @@ -1,6 +1,6 @@ { "name": "pulseengine-claude", - "version": "0.14.0", + "version": "0.14.1", "description": "PulseEngine methodology as installable Claude Code tooling — philosophy + toolchain + repo-taxonomy + model-operating-contract memory, memory-persistence hooks (situational awareness at session start, working-context checkpoints across sessions/compaction), plus fifteen procedural skills (clean-room verification, release execution with a V-model traceability gate, oracle-gating, the full feature loop, the standardized release-artifact pipeline, tool-friction reporting, session-learning capture, STPA/STPA-Sec hazard-analysis audit, backend-agnostic proof synthesis, full bidirectional traceability audit across the V, greenfield verification bootstrap, release planning with an issue-driven delivery loop, an incremental issue-hunt loop, and a quiesce-gated post-release repo-hygiene sweep).", "author": { "name": "PulseEngine", diff --git a/claude-tooling/plugins/pulseengine-claude/skills/proof-synthesis/SKILL.md b/claude-tooling/plugins/pulseengine-claude/skills/proof-synthesis/SKILL.md index e9aac47..d75ee8b 100644 --- a/claude-tooling/plugins/pulseengine-claude/skills/proof-synthesis/SKILL.md +++ b/claude-tooling/plugins/pulseengine-claude/skills/proof-synthesis/SKILL.md @@ -3,7 +3,7 @@ name: proof-synthesis description: This skill should be used when writing, repairing, or strengthening a machine-checked proof, spec, contract, or invariant in ANY PulseEngine verification backend — Verus (SMT/Z3), Rocq/Coq, Lean 4, Dafny, Kani (bounded model checking), or scry (sound abstract interpretation) — and whenever a proof obligation, assertion, or verification job is failing and needs an iterative generate→verify→refine loop. Backend-agnostic by design: the verifier's own output is the oracle, never an LLM's opinion. Fires across gale, scry, the rules_* proof toolchains, and any repo that carries proofs. Use it for the production of proofs; pair it with oracle-gate-a-change (the verifier is the gate) and stpa-audit/feature-loop (which say *what* must be proven). metadata: author: pulseengine.eu - version: "0.4.0" + version: "0.4.1" --- # Proof synthesis @@ -30,8 +30,9 @@ subagents ([`clean-room-verification`]), rather than trusting your own running t 1. **Specify first.** Write the property/contract/invariant *before* the proof. This is the hard part and the usual failure point: on CLEVER (161 Lean - problems) no SOTA agent end-to-end-verifies more than **1**, with - *spec-equivalence* the dominant wall ([arXiv 2505.13938](https://arxiv.org/pdf/2505.13938)). + problems, each demanding a proven-equivalent spec *and* a verified impl) SOTA + agents "struggle to achieve full verification," with getting the **spec** right + — not the proof — a first-class hard task ([arXiv 2505.13938](https://arxiv.org/pdf/2505.13938)). A proof of the wrong spec is worse than no proof. Have the spec itself reviewed cold ([`clean-room-verification`]) — "is this the property we actually need?" — before sinking effort into proving it. @@ -60,7 +61,7 @@ It is the concrete instantiation of [`oracle-gate-a-change`] for proofs. |---|---|---|---| | **Verus** | `cargo verus verify` / `verus` | SMT failure, failing `ensures`/`requires`, timeout | watch quantifier triggers; split lemmas when Z3 times out | | **Rocq / Coq** | `rocq`/`coqc`, `dune build` | remaining proof goal / tactic failure | decide *when to query the prover vs. predict a tactic*, keep a proof-tree (AutoRocq, [arXiv 2511.17330](https://arxiv.org/pdf/2511.17330)) | -| **Lean 4** | `lake build` / `lean` | unsolved goals, `sorry` left | autoformalize NL→spec as a *biconditional* and prove equivalence ([arXiv 2511.11829](https://arxiv.org/pdf/2511.11829)) | +| **Lean 4** | `lake build` / `lean` | unsolved goals, `sorry` left | autoformalize NL→spec, then *prove it equivalent* to the intended spec — not just plausible (CLEVER's spec-match task, [arXiv 2505.13938](https://arxiv.org/pdf/2505.13938)) | | **Dafny** | `dafny verify` | failing assertion / postcondition | strong source for cross-language bootstrap (below) | | **Kani** | `cargo kani` | counterexample trace | bounded — record the bound; absence of CEX ≠ unbounded proof | | **scry** | the abstract-interpretation run | unproven invariant / lost precision | soundness is the property; widening/narrowing tuning is the "refine" step |