kotaroyamame

kotaroyamame/formal-agent-contracts

Plugin Claude Code

Plugin marketplace listing 1 plugin: formal-agent-contracts.

kotaroyamame/formal-agent-contracts

Plugin Claude Code

Formal methods toolkit for multi-agent development: define agent contracts in VDM-SL, generate Phase 2 design documents (PROTOCOL.md, API-SIGNATURES.md), verify specifications, auto-prove with Z3, derive database schemas (DDL) with deviation tracking and invariant traceability, generate code scaffolds with runtime…

kotaroyamame/formal-agent-contracts

Skill Claude CodeCodex

A formal way to define how software agents share responsibilities, data, and messages. It uses VDM-SL, a precise language for describing rules and data, and can produce protocol and API design documents.

kotaroyamame/formal-agent-contracts

Skill Claude CodeCodex

Generate a human-readable natural language specification document (Markdown) from a VDM-SL formal specification. Translates types, invariants, pre/post-conditions, and operations into clear prose that domain experts, project managers, and non-technical stakeholders can understand and review — without needing to learn…

kotaroyamame/formal-agent-contracts

Skill Claude CodeCodex

Extract a provisional VDM-SL specification from existing source code. This is NOT the true spec — it is a scaffold for dialogue to uncover the user's real intent. Triggered by: "extract spec from code", "reverse engineer the specification", "extract-spec", "code to spec", "formalize the existing code". Japanese…

kotaroyamame/formal-agent-contracts

Skill Claude CodeCodex

Provide reference knowledge on VDM-SL and formal methods. Triggered by "VDM-SL syntax", "how to write types", "what is a pre-condition", "what is an invariant", "meaning of proof obligations", "what are formal methods", or "formal specification". Also responds to Japanese: 「VDM-SLの文法」「事前条件とは」「形式手法とは」等。 Referenced as…

kotaroyamame/formal-agent-contracts

Skill Claude CodeCodex

Generate TypeScript/Python code scaffolds from VDM-SL specifications. Triggered by "generate code from the spec", "convert to TypeScript", "generate Python code", "create a scaffold", "generate implementation template", "create type definitions from VDM", or "generate agent code". Also responds to Japanese…

kotaroyamame/formal-agent-contracts

Skill Claude CodeCodex

A method for deriving SQL database table definitions from a VDM-SL specification, a formal description of data, rules, and operations. It records where the database cannot represent a rule exactly.

kotaroyamame/formal-agent-contracts

Skill Claude CodeCodex

A test-generation skill that turns VDM-SL specifications and protocol documents into Jest- or Vitest-compatible contract tests. VDM-SL is a formal language for describing software rules; contract tests check that code follows those rules.

kotaroyamame/formal-agent-contracts

Skill Claude CodeCodex

Import a natural language specification document (Markdown) and interactively convert it to a VDM-SL formal specification. Reads the MD file, identifies requirements, flags ambiguities, and guides the user through a dialogue to fill gaps — producing a complete .vdmsl file. Use this skill whenever the user wants to…

kotaroyamame/formal-agent-contracts

Skill Claude CodeCodex

Orchestrate the full formal development pipeline end-to-end: Define (VDM-SL contract) → Verify (VDMJ) → Prove (Z3, optional) → Generate (TS/Python code) → Test (contract tests), with automated handoff between phases, error recovery, and a final session report. Each phase invokes an existing skill (define-contract…

kotaroyamame/formal-agent-contracts

Skill Claude CodeCodex

Reconcile existing code with the confirmed VDM-SL specification. Compare spec vs code item-by-item, generate a diff report, produce code fixes prioritized by Finding category, and auto-generate tests. Triggered by: "reconcile code with spec", "fix code to match spec", 「仕様とコードを照合して」「コードを仕様に合わせて」「差分を出して」「コードを直して」.

kotaroyamame/formal-agent-contracts

Skill Claude CodeCodex

Refine a provisional VDM-SL specification through dialogue with the user, uncovering the true specification that exists in the user's mind. The provisional spec (from extract-spec) serves as a scaffold for questions. Triggered by: "refine the spec", "review the provisional spec"…

kotaroyamame/formal-agent-contracts

Skill Claude CodeCodex

Orchestrate the full reverse engineering pipeline: Extract provisional spec from existing code, refine through dialogue to uncover the true spec, then reconcile code with the confirmed spec. Optionally connects to the forward pipeline (verify → prove → generate → test). Triggered by: "reverse workflow", "extract and…

kotaroyamame/formal-agent-contracts

Skill Claude CodeCodex

Assign each VDM-SL module to the lightest capable model tier (light / standard / heavy) based on objective complexity signals in the contract itself — operation counts, implicit definitions, state invariants, quantifiers, and proof-obligation counts — to cut token cost without weakening the verification safety net.…

kotaroyamame/formal-agent-contracts

Skill Claude CodeCodex

Convert VDM-SL proof obligations (POs) to SMT-LIB and verify them with the Z3 solver. Triggered by "prove POs", "verify with SMT", "check with Z3", "auto-verify proof obligations", "prove the spec is correct", or "find counterexamples". Also responds to Japanese: 「POを証明して」「SMTで検証して」「Z3で確認して」等。 Used as the next step…

kotaroyamame/formal-agent-contracts

Skill Claude CodeCodex

A checker for VDM-SL, a formal language used to describe software designs precisely. It checks the file’s grammar and types, reviews related design documents, and creates proof obligations—conditions that still need to be proven.