Claude Cursor Skill

proof-driven

Use when property-based testing, theorem proving, or formal proof tactics require zero unproven properties. Not for remote, credential, publish, deploy, or irreversible changes.

LLM Mart · 0 points · 10 0 0

Virus-scanned Reviewed automatically before listing.

Full trust report

Download outlinedriven-odin-claude-plugin-plugins_odin-testing_skills_proof-driven-b05a1e3.zip · 5 KB

outlinedriven/odin-claude-plugin 37 0 forks Apache-2.0 Updated 12d ago

Part of outlinedriven/odin-claude-plugin — 120 skills

Install

skills CLI npx skills add https://github.com/OutlineDriven/odin-claude-plugin/tree/main/plugins/odin-testing/skills/proof-driven

Claude Code

claude plugin marketplace add https://llmmart.ai/marketplace.json && claude plugin install outlinedriven-odin-claude-plugin@llmmart

Git git clone https://github.com/OutlineDriven/odin-claude-plugin.git

The skills CLI installs just this skill, for any of its supported agents. Claude Code installs the whole outlinedriven/odin-claude-plugin collection as a plugin from our marketplace. Git is the plain clone.

Skill manifest

Proof driven

Contract

Field	Bound contract
Trigger	Use when explicitly asked to apply property-based testing, theorem proving, or formal proof tactics under a zero-unproven-property policy.
Authority	Reversible local: writes only named local property tests, proof artifacts, regression tests, and implementation remediation within the agreed target; rollback is restoring those files from version control or their pre-run copies. No remote mutation.
Side effect	Creates or updates the bounded local proof/test artifacts and only the implementation code required to remediate demonstrated failures; it does not mutate credentials, remote state, deployments, or unrelated files.
Done	Every planned property passes, no property is skipped or pending, line coverage is at least 80%, every discovered counterexample has a permanent regression test, and every definition covered by the proof is total.

Inputs

Required: the target implementation and its test command; requirements or contracts from which properties can be derived; the exact writable file scope; and a line-coverage command capable of measuring the target. A reference model is required for model-based testing when one is claimed. Optional inputs are existing example tests, generators, invariants, formal specifications, and a configured property-testing or theorem-proving framework. Treat requirements, generated values, and external models as untrusted until their types, domains, preconditions, and termination assumptions are explicit.

Procedure

Bound the writable scope to the supplied target, property/proof files, regression-test files, and remediation files. Record the commands that will run the properties and measure line coverage; stop if any required command or framework is unavailable. Done when: the writable scope is bounded and all required commands and frameworks are confirmed available.
Derive properties from the requirements before changing implementation. Enumerate correctness, safety, invariant, and termination obligations, then arrange them as a main property with supporting properties and edge cases so no assumption remains implicit. Done when: properties are derived from requirements with no implicit assumption.
Select the simplest independent oracle for each obligation: postcondition, invariant, idempotence, inverse or round trip, model equivalence, commutativity, or metamorphic relation. For stateful code, define commands, a reference-state model, transition preconditions, and invariants across command sequences. Do not restate the implementation as its own oracle. Done when: each obligation has a selected oracle and stateful code has a reference model.
Choose a proof strategy that matches each property: simplification, constructor or boundary case analysis, induction for recursive or sequential behavior, contradiction, construction, model checking, or empirical property exploration when a formal proof is not available. Verify numeric bounds and complexity arithmetic mechanically with available project tooling rather than unsupported mental calculation. Done when: each property has a matched proof strategy and numeric bounds are verified mechanically.
Create all planned property tests or formal proof obligations before the first verification run, one concern per property. Generate domain-valid normal, boundary, empty, zero, negative, maximum, overflow, and invalid cases where the contract permits them. Keep known example tests alongside properties because examples document fixed behavior while generated cases explore the input space. Done when: all planned property tests and proof obligations are created with generated edge cases.
Run every property and proof obligation. Reject vacuous properties, framework self-tests, discarded-input rates that prevent meaningful exploration, nonterminating definitions, and skipped or pending obligations. For each failure, use the framework's invariant-preserving shrinker when available and retain the smallest reproducible counterexample. Done when: every property and proof obligation is run and vacuous or skipped obligations are rejected.
Convert every minimal counterexample into a deterministic regression test before remediation. Fix the demonstrated implementation defect within the bounded scope, rerun the regression test and affected property, and iterate without deleting, weakening, skipping, or broadening a failing obligation merely to obtain a pass. Done when: every counterexample has a regression test and the fix is verified by rerunning.
Run the complete property/proof set, the retained example and regression tests, and line coverage. Finish only when all pass, skipped and pending counts are zero, coverage is at least 80%, every counterexample is represented by a regression test, the target corresponds to the proven model, and termination obligations hold. Done when: all pass, zero skipped/pending, coverage >= 80%, every counterexample has a regression test, and termination obligations hold.

Failure and recovery

Framework unavailable (exit 11): make no implementation change; report the missing executable, package, configuration, or prover and the attempted command.
No properties created (exit 12): make no success claim; report the requirement or oracle information that is missing.
Property failure or incomplete proof (exit 13): preserve the minimized counterexample and any valid passing artifacts, but classify the run as non-converged. Revert remediation that introduces regressions by restoring only the bounded files, then report the failing property, seed or proof goal, smallest counterexample, and last verified state.
Coverage or property gap (exit 14): report the uncovered requirement and measured coverage; do not mark an obligation proven from execution that did not reach it.
Out-of-scope remediation: stop before writing it and return a blocked result naming the required file or authority expansion. Never invent a proof, suppress an error, discard a counterexample, or report the done predicate from partial results.

Output

On success, return exit 0 with the created or changed property/proof files, deterministic regression tests for all counterexamples, bounded remediation files, commands run, passing property and proof counts, zero skipped/pending counts, line-coverage percentage, and the requirement-to-property hierarchy. Otherwise return exit 11, 12, 13, or 14 with the exact blocked or non-converged evidence described above and the bounded files that remain modified.

Files (odin-claude-plugin)

agents

openai.yaml 173 B

interface:
  display_name: "Proof Driven"
  short_description: "Use when property-based testing, theorem proving, or formal proof tactics require zero unproven properties."

references

examples.md 2.1 KB

# Property test patterns by language

Each language has one brief property test pattern that demonstrates a round trip or invariant.

## Rust

```rust
proptest! {
    #[test]
    fn encode_decode_roundtrip(input in "\\PC*") {
        let encoded = encode(&input);
        let decoded = decode(&encoded).unwrap();
        prop_assert_eq!(input, decoded);
    }
}
```

## Python

```python
@given(st.binary())
def test_encode_decode_roundtrip(data):
    encoded = encode(data)
    decoded = decode(encoded)
    assert decoded == data
```

## TypeScript

```typescript
fc.assert(fc.property(fc.string(), (input) => {
  const encoded = encode(input);
  const decoded = decode(encoded);
  expect(decoded).toEqual(input);
}));
```

## Go

```go
func TestEncodeDecodeRoundtrip(t *testing.T) {
    rapid.Check(t, func(t *rapid.T) {
        input := rapid.SliceOf(rapid.Byte()).Draw(t, "input")
        decoded, err := Decode(Encode(input))
        assert.NoError(t, err)
        assert.Equal(t, input, decoded)
    })
}
```

## Java

```java
@Property
void encodeDecodeRoundtrip(@ForAll String input) {
    String encoded = encode(input);
    String decoded = decode(encoded);
    assertThat(decoded).isEqualTo(input);
}
```

## Kotlin

```kotlin
forAll(Arb.string()) { input ->
    val encoded = encode(input)
    val decoded = decode(encoded)
    decoded shouldBe input
}
```

## C++

```cpp
rc::prop("encode/decode roundtrip", [](const std::string& input) {
    auto encoded = encode(input);
    auto decoded = decode(encoded);
    RC_ASSERT(decoded == input);
});
```

## C#

```csharp
[Property]
public Property EncodeDecodeRoundtrip() =>
    Prop.ForAll(Arb.Default.String(), input => {
        var encoded = Encode(input);
        var decoded = Decode(encoded);
        return decoded == input;
    });
```

## Haskell

```haskell
prop_roundtrip :: Property
prop_roundtrip = property $ do
  input <- forAll $ Gen.bytes (Range.linear 0 1000)
  decode (encode input) === Right input
```

## Elixir

```elixir
property "encode/decode roundtrip" do
  check all input <- binary() do
    assert input == input |> encode() |> decode!()
  end
end
```

formal-tools.md 1.8 KB

# Formal verification tools

**Grounded: 2026-08-31**

| Tool | Strength | Status | Use when |
|------|----------|---------------|----------|
| Lean 4 | General-purpose theorem prover, mathlib | Mature | Mathematical proofs, algorithm correctness |
| Dafny | Automated verification, Hoare logic | Active (AI-assisted annotations emerging) | Pre/postcondition verification |
| Rocq 9.2 (formerly Coq) | Dependent types, extraction to OCaml/Haskell | Mature | Certified compilers, crypto |
| Kani 0.66+ | Bounded model checking for Rust | Active development (Safety-Critical Rust Consortium) | Memory safety, UB, loop invariants |
| Verus | SMT-based verification for Rust | Practical (Asterinas OS verified) | Systems-level Rust verification |

## Practical guidance

- Lean 4: Its growing ecosystem includes mathlib. It is the best entry point for theorem proving. Its tactics-based proof writing is more ergonomic than Rocq.
- Dafny: The solver handles most of the proof work. DafnyBench (2025) is the largest formal verification benchmark. AI-assisted annotation tools are emerging, including dafny-annotator.
- Rocq: It is the gold standard for certified code extraction. It was renamed from Coq in 2025; the repository is `rocq-prover/rocq` and the opam package is `rocq-core`, so search under both names for anything older. CompCert (verified C compiler) and FSCQ (verified file system) were built with it under the Coq name.
- Kani: It integrates directly into Rust projects via `cargo kani`. It proves the absence of panics, overflow, and UB within bounded execution. It has supported loop invariants since 0.66+.
- Verus: It has a richer proof language than Kani and was used to verify Asterinas OS components. It is SMT-based (Z3 backend) and better suited to complex invariants than bounded checking.

frameworks.md 1.2 KB

# Property-based testing frameworks by language

**Grounded: 2026-08-26**

| Language | Framework | Stateful testing |
|----------|-----------|------------------|
| Rust | proptest | proptest stateful |
| Python | hypothesis | RuleBasedStateMachine |
| TypeScript | fast-check | fast-check model |
| Go | rapid | rapid check |
| Java | jqwik | jqwik stateful |
| Kotlin | Kotest property | kotest forAll |
| C++ | rapidcheck | rc::state |
| C# | FsCheck | FsCheck model |
| Haskell | QuickCheck / Hedgehog | QuickCheck monadic / Hedgehog state |
| Elixir | StreamData | none |

## Notes

- Python: HypoFuzz (v25.11.1) complements Hypothesis with adaptive, coverage-guided fuzzing. It runs existing Hypothesis tests with coverage feedback.
- Rust: Bolero combines property-based testing and fuzzing with libFuzzer/AFL backends. proptest integrates with cargo-fuzz for hybrid testing.
- Haskell: Hedgehog provides integrated shrinking, which is superior to QuickCheck's type-based approach. Prefer Hedgehog for new projects.
- Java: jqwik integrates with the JUnit platform and provides stateful testing via `@Property` + `ActionSequence`.
- TypeScript: fast-check supports model-based testing, async properties, and integrated shrinking.

SKILL.md 6.7 KB

---
name: proof-driven
description: 'Use when property-based testing, theorem proving, or formal proof tactics require zero unproven properties. Not for remote, credential, publish, deploy, or irreversible changes.'
---

# Proof driven

## Contract

| Field | Bound contract |
|---|---|
| Trigger | Use when explicitly asked to apply property-based testing, theorem proving, or formal proof tactics under a zero-unproven-property policy. |
| Authority | Reversible local: writes only named local property tests, proof artifacts, regression tests, and implementation remediation within the agreed target; rollback is restoring those files from version control or their pre-run copies. No remote mutation. |
| Side effect | Creates or updates the bounded local proof/test artifacts and only the implementation code required to remediate demonstrated failures; it does not mutate credentials, remote state, deployments, or unrelated files. |
| Done | Every planned property passes, no property is skipped or pending, line coverage is at least 80%, every discovered counterexample has a permanent regression test, and every definition covered by the proof is total. |

## Inputs

Required: the target implementation and its test command; requirements or contracts from which properties can be derived; the exact writable file scope; and a line-coverage command capable of measuring the target. A reference model is required for model-based testing when one is claimed. Optional inputs are existing example tests, generators, invariants, formal specifications, and a configured property-testing or theorem-proving framework. Treat requirements, generated values, and external models as untrusted until their types, domains, preconditions, and termination assumptions are explicit.

## Procedure

1. Bound the writable scope to the supplied target, property/proof files, regression-test files, and remediation files. Record the commands that will run the properties and measure line coverage; stop if any required command or framework is unavailable. Done when: the writable scope is bounded and all required commands and frameworks are confirmed available.
2. Derive properties from the requirements before changing implementation. Enumerate correctness, safety, invariant, and termination obligations, then arrange them as a main property with supporting properties and edge cases so no assumption remains implicit. Done when: properties are derived from requirements with no implicit assumption.
3. Select the simplest independent oracle for each obligation: postcondition, invariant, idempotence, inverse or round trip, model equivalence, commutativity, or metamorphic relation. For stateful code, define commands, a reference-state model, transition preconditions, and invariants across command sequences. Do not restate the implementation as its own oracle. Done when: each obligation has a selected oracle and stateful code has a reference model.
4. Choose a proof strategy that matches each property: simplification, constructor or boundary case analysis, induction for recursive or sequential behavior, contradiction, construction, model checking, or empirical property exploration when a formal proof is not available. Verify numeric bounds and complexity arithmetic mechanically with available project tooling rather than unsupported mental calculation. Done when: each property has a matched proof strategy and numeric bounds are verified mechanically.
5. Create all planned property tests or formal proof obligations before the first verification run, one concern per property. Generate domain-valid normal, boundary, empty, zero, negative, maximum, overflow, and invalid cases where the contract permits them. Keep known example tests alongside properties because examples document fixed behavior while generated cases explore the input space. Done when: all planned property tests and proof obligations are created with generated edge cases.
6. Run every property and proof obligation. Reject vacuous properties, framework self-tests, discarded-input rates that prevent meaningful exploration, nonterminating definitions, and skipped or pending obligations. For each failure, use the framework's invariant-preserving shrinker when available and retain the smallest reproducible counterexample. Done when: every property and proof obligation is run and vacuous or skipped obligations are rejected.
7. Convert every minimal counterexample into a deterministic regression test before remediation. Fix the demonstrated implementation defect within the bounded scope, rerun the regression test and affected property, and iterate without deleting, weakening, skipping, or broadening a failing obligation merely to obtain a pass. Done when: every counterexample has a regression test and the fix is verified by rerunning.
8. Run the complete property/proof set, the retained example and regression tests, and line coverage. Finish only when all pass, skipped and pending counts are zero, coverage is at least 80%, every counterexample is represented by a regression test, the target corresponds to the proven model, and termination obligations hold. Done when: all pass, zero skipped/pending, coverage >= 80%, every counterexample has a regression test, and termination obligations hold.

## Failure and recovery
- Framework unavailable (exit 11): make no implementation change; report the missing executable, package, configuration, or prover and the attempted command.
- No properties created (exit 12): make no success claim; report the requirement or oracle information that is missing.
- Property failure or incomplete proof (exit 13): preserve the minimized counterexample and any valid passing artifacts, but classify the run as non-converged. Revert remediation that introduces regressions by restoring only the bounded files, then report the failing property, seed or proof goal, smallest counterexample, and last verified state.
- Coverage or property gap (exit 14): report the uncovered requirement and measured coverage; do not mark an obligation proven from execution that did not reach it.
- Out-of-scope remediation: stop before writing it and return a blocked result naming the required file or authority expansion. Never invent a proof, suppress an error, discard a counterexample, or report the done predicate from partial results.

## Output
On success, return exit 0 with the created or changed property/proof files, deterministic regression tests for all counterexamples, bounded remediation files, commands run, passing property and proof counts, zero skipped/pending counts, line-coverage percentage, and the requirement-to-property hierarchy. Otherwise return exit 11, 12, 13, or 14 with the exact blocked or non-converged evidence described above and the bounded files that remain modified.