lean-conformance

Property-based spec<->code conformance for this repo — regenerate Lean-emitted vectors (lake exe vectorgen), replay them against Recovery.Logic with the Haskell tasty-hedgehog suite, and run the mutation sweep (each single-guard mutation must fail at least one vector). Use when validating that the Lean spec still verifies the Haskell implementation, or when the review council's fidelity/adversarial lenses need conformance evidence.

Zur Installation springen

Repository: CharlesHoskinson/proof-zk-recovery
Letzte Quellaktivität: 30. Juni 2026 um 16:04
Erkannte Sprache von SKILL.md: Englisch
Sterne: 17
Forks: 6

Installationsoptionen

Standardmäßig ist der Prompt ausgewählt, der zuerst die Quelle prüft. Sie können zu einem direkten Befehl wechseln oder eine lokale Kopie herunterladen.

Mit Codex oder Claude installieren Kopieren Sie diesen Prompt, fügen Sie ihn in Codex, Claude oder einen anderen Assistant ein und lassen Sie die Skill-Seite prüfen und installieren.

Ein direkter Befehl überspringt den Prüf-Prompt. Prüfen Sie die Quelle, bevor Sie ihn ausführen.

npx skills add https://github.com/CharlesHoskinson/proof-zk-recovery --skill lean-conformance

Der Befehl bleibt in einer Zeile. Scrollen Sie horizontal, um ihn vor dem Kopieren vollständig zu prüfen.

Sie bevorzugen eine lokale Kopie? Laden Sie die Dateien herunter, die SkillsMP derzeit vorliegen.

Quelldateien prüfen

Lesen Sie SKILL.md und alle von SkillsMP angezeigten Begleitdateien, bevor Sie sich für eine Installation entscheiden.

Datei-Explorer

6 Dateien

SKILL.md

Quellanweisungen · Schreibgeschützte Vorschau

Zurück zur Suche Zurück zur Installation

vibesec

Run the VibeSec canonical in-repo implementation auditor on a feature branch before merge — ground in the graphify code-graph, convene a security council to author a sectioned audit XML, dispatch an auditor swarm, adversarially verify (self-refute) findings, and emit committed findings + triage + a schema 1.2 machine-readable gate report. Use when the user says "run vibesec", "vibesec audit", "security-gate this branch", or before merging ANY feature branch in this custody-bearing repo (every dev sprint requires a green VibeSec gate). The gate is enforced in CI (.github/workflows/vibesec.yml).

2026-07-02

lean-review

Run the per-phase Lean review-council QA gate on the lean-spec-enhancement work — a tool-executing council of four expert lenses (axiom-hygiene guardian, spec<->code fidelity, proof nonvacuity, adversarial red-team) that build the proofs, run

2026-07-01

lean-prove

Interactive Lean 4 proof development for this repo — the sorrify-then-fill loop driven over lean-lsp-mcp (goal state, diagnostics, Loogle search), with Duper/lean-auto escalation and a hard

2026-06-30

Alle aus diesem Repository ansehen

name	lean-conformance
description	Property-based spec<->code conformance for this repo — regenerate Lean-emitted vectors (lake exe vectorgen), replay them against Recovery.Logic with the Haskell tasty-hedgehog suite, and run the mutation sweep (each single-guard mutation must fail at least one vector). Use when validating that the Lean spec still verifies the Haskell implementation, or when the review council's fidelity/adversarial lenses need conformance evidence.
argument-hint	[regen \| run \| mutate]