odin-formal

Plugin odin-formal from marketplace odin-marketplace in OutlineDriven/odin-claude-plugin. Commands read from the repo's manifest — 1 month ago.

Skills (9)

• bounded-model-checking-c

  Use when C or C++ code needs memory-safety or undefined-behavior guarantees proved with CBMC, or ACSL contracts checked with Frama-C Eva or WP. Not for choosing the proof policy: use proof-driven.

• deductive-verification-with-dafny-and-why3

  Use when an imperative program needs pre-conditions, post-conditions, and loop invariants proved automatically by SMT in Dafny or Why3, short of a tactic prover.

• f-star-effectful-verification

  Use when effectful, security-sensitive code needs refinement-typed, SMT-backed verification in F*, in the HACL* or Project Everest style.

• rust-formal-verification

  Use when Rust code, especially unsafe or panic-critical paths, needs a Kani, Verus, or Creusot harness written, run, and its failure read. Not for choosing the proof policy: use proof-driven.

• smt-solving-with-z3-cvc5

  Use when a query needs direct SMT solving, an unsat core needs debugging, or another tool reports a solver timeout or unknown. Not for deciding what to prove: use proof-driven.

• writing-isabelle-proofs

  Use when a proof needs Isabelle/HOL, its Sledgehammer automation, or an AFP session. Not for Lean 4: use writing-lean-proofs.

• writing-lean-proofs

  Use when asked to design, write, review, refactor, lint, or performance-diagnose Lean 4 proofs, libraries, or tactics. Not for non-Lean code or changes outside source, API, proof, or linter scope.

• writing-rocq-proofs

  Use when a proof needs Rocq (formerly Coq), including legacy Coq codebase maintenance and migration through the Coq to Rocq rename. Not for Lean 4: use writing-lean-proofs.

• writing-tla-plus-specs

  Use when a protocol, concurrent algorithm, or design needs a model-checked TLA+ or Alloy spec, or a TLC or Apalache trace needs reading. Not for choosing when to model: use validation-first-driven.

Similar plugins