스킬 찾기

Translate Python programs to equivalent Lean4 code while preserving semantics and ensuring type safety. Use when users ask to convert, translate, or port Python code to Lean4, or when they need to verify Python algorithms using Lean4's theorem proving capabilities. Handles functions, classes, data structures, control flow, and ensures the generated Lean4 code is well-typed, executable, and can successfully run.

한국어 요약은 준비 중입니다. 원문 설명을 표시하고 있습니다.

Systematic external reference searching across documentation, open-source repositories, and web resources. Use when working with unfamiliar libraries, APIs, or when needing production-quality implementation examples.

한국어 요약은 준비 중입니다. 원문 설명을 표시하고 있습니다.

Generate systematic refinement steps from high-level specifications to concrete implementations in Isabelle/HOL or Coq, preserving correctness obligations at each step. Use when working with formal verification, program refinement, proof development, or when translating abstract specifications into executable code while maintaining formal guarantees. Supports data refinement (abstract types → concrete structures), algorithmic refinement (specifications → algorithms), and stepwise refinement with proof obligations.

한국어 요약은 준비 중입니다. 원문 설명을 표시하고 있습니다.

Locate root causes of failing regression tests by analyzing code changes, error messages, and test dependencies. Use when regression tests start failing after code changes, investigating test failures in CI/CD, debugging flaky tests, or understanding why previously passing tests now fail. Analyzes git diffs, stack traces, test output, and dependency changes to produce structured markdown reports ranking likely causes. Triggers when users ask to find why tests are failing, debug regression failures, investigate test breakage, or analyze failing test suites.

한국어 요약은 준비 중입니다. 원문 설명을 표시하고 있습니다.

Automatically generate user-facing release notes from git commits, pull requests, changelogs, and code changes. Use when preparing software releases, creating version announcements, documenting what changed between versions, or communicating updates to users. Analyzes commit messages, PR descriptions, and code diffs to produce categorized markdown release notes organized by New Features, Improvements, Bug Fixes, and Breaking Changes. Focuses on user-visible changes while filtering out internal/technical details. Triggers when users ask to generate release notes, create changelog, write version announcement, or summarize changes for a release.

한국어 요약은 준비 중입니다. 원문 설명을 표시하고 있습니다.

Instruments programs to record execution information for deterministic replay debugging. Use when debugging hard-to-reproduce bugs (race conditions, timing issues, intermittent failures, heisenbugs), reproducing production failures, or analyzing complex execution sequences. Records non-deterministic events (I/O, threading, randomness, time) to enable exact replay of program executions. Supports Python, JavaScript, Java, and C/C++ with both custom instrumentation and existing replay tools.

한국어 요약은 준비 중입니다. 원문 설명을 표시하고 있습니다.

Generates comprehensive test scenarios from requirements including BDD/Gherkin scenarios, unit tests, integration tests, and end-to-end test cases. Use when converting requirements, user stories, or specifications into testable scenarios with full coverage including happy paths, error cases, edge cases, and boundary conditions. Outputs structured test suites ready for implementation.

한국어 요약은 준비 중입니다. 원문 설명을 표시하고 있습니다.

Compares old and new requirement documents, analyzes code repository impact, and generates detailed modification plans. Use when Claude needs to: (1) Compare requirement versions and identify changes, (2) Map requirement changes to code components, (3) Identify components to modify, delete, or add, (4) Analyze dependencies and integration points, (5) Assess test impact, (6) Generate comprehensive modification plans in Markdown format. Supports text/Markdown requirements and analyzes feature-level, functional, and API changes.

한국어 요약은 준비 중입니다. 원문 설명을 표시하고 있습니다.

Iteratively enhance user requirements into clear, complete, actionable specifications through analysis and clarification. Use when: (1) Users provide initial requirements that need refinement, (2) Requirements are vague, incomplete, or ambiguous, (3) Creating formal specifications from informal descriptions, (4) Identifying missing constraints, edge cases, or acceptance criteria, (5) Clarifying assumptions and implicit dependencies, or (6) Preparing requirements for design, implementation, or verification. Operates interactively: analyze → ask clarifying questions → refine based on responses.

한국어 요약은 준비 중입니다. 원문 설명을 표시하고 있습니다.

Generate concise, structured summaries of requirements for quick team understanding. Use when analyzing requirements from text documents (MD, TXT, DOCX) or technical specifications to create bullet-point summaries that highlight core functionality and dependencies/constraints. Ideal for sprint planning, stakeholder updates, team onboarding, or any situation requiring rapid comprehension of requirement documents.

한국어 요약은 준비 중입니다. 원문 설명을 표시하고 있습니다.

Automatically derives TLA+ properties (invariants, safety, liveness) from natural-language requirements or structured requirement documents. Resolves ambiguities, asks clarifying questions for underspecified requirements, and outputs TLA+-compatible property definitions with semantic explanations. Use when translating system requirements, specifications, or behavioral constraints into formal TLA+ temporal logic properties for verification with TLC model checker.

한국어 요약은 준비 중입니다. 원문 설명을 표시하고 있습니다.

Hardware verification tool for checking functional equivalence between two RTL designs (Verilog). Use when users need to: (1) Verify if two RTL versions are functionally equivalent, (2) Compare original vs. refactored RTL code, (3) Validate design changes or optimizations, (4) Identify semantic vs. cosmetic differences, (5) Generate counterexamples for non-equivalent designs. Analyzes interface alignment, state variables, logic differences, and produces detailed equivalence verdicts with plain language explanations. Particularly effective for design verification, code reviews, and regression testing of RTL modifications.

한국어 요약은 준비 중입니다. 원문 설명을 표시하고 있습니다.

Automatically infer formal correctness properties from Verilog/SystemVerilog RTL code and generate SystemVerilog Assertions (SVA). Identifies control-flow invariants (mutual exclusion, valid-ready handshakes, pipeline ordering, safety properties), liveness expectations, and temporal properties. Use when working with RTL designs that need formal property generation, when adding assertions to existing RTL, or when users ask to infer properties, generate assertions, or create formal specifications from hardware designs.

한국어 요약은 준비 중입니다. 원문 설명을 표시하고 있습니다.

Automatically extract abstract finite-state models in SMV/NuSMV format from source code (C/C++, Java, Python) for formal model checking. Use when users need to: (1) Generate SMV models from program code for verification, (2) Extract state-transition models from protocol implementations, (3) Analyze control flow and data flow to construct formal models, (4) Create models for checking safety and liveness properties, (5) Convert imperative code to declarative state machines. Particularly effective for protocol implementations, concurrent systems, and control logic with clear state transitions.

한국어 요약은 준비 중입니다. 원문 설명을 표시하고 있습니다.

Guide for creating effective skills. This skill should be used when users want to create a new skill (or update an existing skill) that extends Claude's capabilities with specialized knowledge, workflows, or tool integrations.

한국어 요약은 준비 중입니다. 원문 설명을 표시하고 있습니다.

Git expert combining atomic commits, rebase/squash, and history search (blame, bisect, log -S). Use for any git operations requiring structured commit strategies, history rewriting, or code archaeology. Triggers: 'commit', 'rebase', 'squash', 'who wrote', 'when was X added', 'find the commit that'.

한국어 요약은 준비 중입니다. 원문 설명을 표시하고 있습니다.

Generate targeted test inputs to reach specific code paths and hard-to-reach behaviors in Python code. Use when: (1) Targeting uncovered branches or specific execution paths, (2) Need coverage-guided test generation, (3) Want to leverage LLM understanding of code semantics for meaningful test inputs, (4) Testing boundary conditions and edge cases systematically, (5) Combining symbolic reasoning with fuzzing. Provides path analysis, constraint solving, coverage-guided strategies, and LLM-driven semantic generation for comprehensive test input creation.

한국어 요약은 준비 중입니다. 원문 설명을 표시하고 있습니다.

Designer-turned-developer who crafts stunning UI/UX even without design mockups. Use for any frontend implementation requiring visual design decisions, aesthetic direction, or pixel-perfect UI work.

한국어 요약은 준비 중입니다. 원문 설명을 표시하고 있습니다.

Takes a Python repository and natural language feature description as input, implements the feature with proper code placement, generates comprehensive tests, and ensures all tests pass. Use when Claude needs to: (1) Add new features to existing Python projects, (2) Implement functions, classes, or modules based on requirements, (3) Modify existing code to add functionality, (4) Generate unit and integration tests for new code, (5) Fix failing tests after implementation, (6) Ensure code follows existing patterns and conventions.

한국어 요약은 준비 중입니다. 원문 설명을 표시하고 있습니다.

Generate integration tests for multiple interacting components in Python. Use when testing interactions between: (1) Multiple services or APIs (REST/GraphQL endpoints, microservices), (2) Database operations with repositories/ORMs (SQLAlchemy, Django ORM), (3) External services (payment gateways, email services, third-party APIs), (4) Message queues and event-driven systems, (5) Full stack workflows (API + database + business logic). Provides test structure templates, fixtures, test data builders, and patterns for pytest-based integration testing.

한국어 요약은 준비 중입니다. 원문 설명을 표시하고 있습니다.

Analyze differences in program intervals between two versions of a program (old and new) to identify added, removed, or modified intervals. Use when comparing program versions, analyzing variable ranges, detecting behavioral changes in numeric computations, validating refactorings, or assessing migration impacts. Supports optional test suite integration to validate interval changes. Generates comprehensive reports highlighting intervals requiring further testing or verification.

한국어 요약은 준비 중입니다. 원문 설명을 표시하고 있습니다.

Reorganizes markdown documents into well-structured, consistent format while preserving content and improving readability. Use when Claude needs to: (1) Fix heading hierarchy issues (skipped levels, multiple h1s), (2) Generate or update table of contents, (3) Standardize formatting (lists, code blocks, emphasis, links), (4) Improve grammar and spelling, (5) Add missing standard sections (installation, usage, etc.), (6) Remove redundant or duplicate content, (7) Restructure technical docs, READMEs, or long-form content for better organization and flow.

한국어 요약은 준비 중입니다. 원문 설명을 표시하고 있습니다.

Generate test cases using metamorphic testing by applying transformations based on metamorphic properties. Use when you need to expand test suites, test programs without oracles, validate mathematical or algorithmic properties, or detect subtle bugs through input-output relationships. The skill takes a program, original test cases, and metamorphic properties as input, generates new test cases by applying transformations, executes tests, verifies outputs satisfy properties, reports violations and anomalies, and outputs an expanded test suite with property coverage summary. Supports multiple programming languages and property types.

한국어 요약은 준비 중입니다. 원문 설명을 표시하고 있습니다.

Automatically repair code violations of temporal properties using model-checking counterexamples as guidance. Use when working with formal verification results, temporal logic property violations (LTL, CTL), model checking counterexamples, or when asked to repair property violations, fix counterexamples, repair temporal properties, fix model checking violations, or repair code based on counterexamples. Applicable to concurrent systems, state machines, synchronization issues, safety/liveness properties, and resource management violations.

한국어 요약은 준비 중입니다. 원문 설명을 표시하고 있습니다.