Skip to content

fix(proof-synthesis): correct two miscited arXiv claims #130

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
avrabe merged 1 commit into from
Jul 15, 2026
Merged

fix(proof-synthesis): correct two miscited arXiv claims #130

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion claude-tooling/plugins/pulseengine-claude/.claude-plugin/plugin.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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",
Expand Down
9 changes: 5 additions & 4 deletions claude-tooling/plugins/pulseengine-claude/skills/proof-synthesis/SKILL.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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.
Expand Down Expand Up @@ -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 |
Expand Down