Skillget

Skills-4-SE

skill
Security Audit
Fail
Health Pass
  • License — License: Apache-2.0
  • Description — Repository has a description
  • Active repo — Last push 0 days ago
  • Community trust — 143 GitHub stars
Code Fail
  • rm -rf — Recursive force deletion command in skill-manager/deploy-to-github.sh
  • network request — Outbound network request in skill-manager/frontend/app.js
Permissions Pass
  • Permissions — No dangerous permissions requested

No AI report is available for this listing yet.

SUMMARY

A curated list of 180+ useful Claude Skills for Software Engineering and resources for customizing AI for SE workflows.

README.md

✨ Skills-4-SE: Useful Skills for Software Engineering

Welcome Contribution
中文
English

This repository is a comprehensive, reusable, task-oriented Skills collection designed to support software engineering activities across the entire development lifecycle, including:

Requirement understanding, system design, implementation, testing, verification, deployment, and maintenance.

We provide:

🌐 Skills Manager Web Interface

🚀 Visit Skills Manager

You can also deploy the website locally. 👉 Guideline

Skills Manager Interface

Browse, search, and install skills through our interactive web interface. The Skills Manager provides:

  • 📦 One-click installation of all skills
  • ✅ Selective installation of specific skills
  • 🔍 Search and filter by category
  • 📖 Bilingual help documentation (English/中文)
  • 🎨 Modern, responsive interface

Skills Manager Interface

📦 Skill Packs

Organized collections of related skills for common software engineering workflows. Instead of installing skills individually, you can install curated skill packs that bundle related capabilities together.

Skills Manager Interface

🚀 Available Skill Packs (8 Total)

Quick Installation

# Install a single pack
cd skill-packs/formal-verification-toolkit
./install.sh

# Install multiple packs
cd skill-packs
./install-packs.sh formal-verification-toolkit security-scanner-suite

# Install all packs
cd skill-packs
./install-all-packs.sh

👉 Learn more about Skill Packs

✨ Why Skills (not just prompts)?

Modern LLMs are powerful, but raw prompting is fragile:

  • Hard to reproduce
  • Hard to evaluate
  • Hard to integrate into real workflows

We treat Skills as first-class engineering artifacts, in preparation for the future metaprogramming.

A Skill in this repo is more than a prompt:

  • It encodes procedural knowledge
  • It specifies expected inputs / outputs
  • It documents failure modes
  • It can be evaluated, composed, and reused

🤗 Think of this repo as a standard library of software engineering capabilities for LLM-powered systems.

List of Skills

Skills by Category

Code Generation

Function/Class Generator

  • Generates functions and classes from specifications
  • Supports multiple programming languages
  • Includes type hints, documentation, and error handling

Module/Component Generator

  • Builds complete modules from interface contracts
  • Generates layered architectures (model, repository, service)
  • Supports Python and Java with design patterns

Template Code Generator

  • Creates boilerplate code from templates
  • Supports common patterns and frameworks
  • Customizable templates for different use cases

Specification-Driven Generation

  • Generates code from formal specifications
  • Ensures specification compliance
  • Validates generated code against requirements

Test-Driven Generation

  • Generates implementation from test cases
  • Follows TDD principles
  • Ensures test coverage

Incremental Python Programmer

  • Implements new features in Python repositories from natural language descriptions
  • Generates comprehensive unit and integration tests
  • Ensures all tests pass and follows existing code patterns

Incremental Java Programmer

  • Implements new features in Java repositories from natural language descriptions
  • Supports Maven and Gradle build systems
  • Generates JUnit tests and ensures all tests pass successfully

Pseudocode Extractor

  • Extracts programming-language-agnostic pseudocode from source code
  • Preserves control flow and logical structure
  • Filters out implementation details for clarity

Module-Level Code Translator

  • Translates source code between programming languages at module level
  • Preserves behavior and adapts to target language idioms
  • Generates verification tests for translated code

Pseudocode to Java Code

  • Converts pseudocode descriptions into complete, executable Java programs
  • Preserves original logic and control flow
  • Applies appropriate Java idioms and best practices

Pseudocode to Python Code

  • Converts pseudocode and algorithm descriptions into executable Python code
  • Provides proper structure, documentation, and tests
  • Maintains algorithmic logic while following Python conventions

Testing

Unit Test Generator

  • Generates unit tests for functions and classes
  • Supports multiple testing frameworks
  • Includes edge cases and assertions

Integration Test Generator

  • Creates integration tests for system components
  • Tests component interactions
  • Includes setup and teardown logic

Java Test Updater

  • Updates Java tests to work with new code versions after refactoring
  • Handles signature changes, refactoring, and behavior modifications
  • Updates method calls, assertions, mocks, and ensures tests pass

Flaky Test Detector

  • Identifies non-deterministic tests
  • Analyzes test execution patterns
  • Suggests fixes for common flaky patterns

Test Oracle Generator

  • Generates expected outputs for test cases
  • Creates assertions and validation logic
  • Supports property-based testing

Edge Case Generator

  • Identifies and generates edge case tests
  • Covers boundary conditions
  • Includes corner cases and error scenarios

Directed Test Input Generator

  • Generates targeted test inputs
  • Focuses on specific code paths
  • Uses symbolic execution techniques

Fuzzing Input Generator

  • Creates randomized test inputs
  • Discovers unexpected behaviors
  • Supports mutation-based fuzzing

Test Suite Prioritizer

  • Prioritizes test execution order
  • Optimizes for early failure detection
  • Considers test dependencies and coverage

Coverage Enhancer

  • Identifies uncovered code paths
  • Generates tests to improve coverage
  • Reports coverage metrics

Test Case Documentation

  • Documents test cases and their purposes
  • Explains test scenarios and expected outcomes
  • Maintains test documentation

Python Test Updater

  • Updates Python tests to work with new code versions
  • Fixes broken tests due to signature and behavior changes
  • Analyzes code diffs and updates assertions accordingly

Bug Reproduction Test Generator

  • Automatically generates tests that reproduce reported bugs from issue reports
  • Analyzes bug symptoms, stack traces, and triggering conditions
  • Creates minimal, focused tests that reliably trigger the bug
  • Supports Python, Java, and JavaScript test frameworks

Interval-Guided Regression Test Update

  • Updates regression tests based on interval analysis

Requirement to Test

  • Converts requirements to test cases
  • Ensures requirement coverage
  • Traces tests back to requirements

Test Case Reducer

  • Reduces test cases to minimal form using delta debugging

Java Regression Test Generator

  • Automatically generates regression tests for Java codebases
  • Analyzes changes between old and new code versions
  • Ensures tests cover refactored or modified functionality

Python Regression Test Generator

  • Automatically generates regression tests for Python codebases
  • Analyzes changes between code versions and migrates existing tests
  • Generates tests for new functionality

Mocking Test Generator

  • Generates unit tests with proper mocking for Python and Java
  • Supports unittest.mock/pytest for Python and Mockito/JUnit for Java
  • Handles external dependencies and complex interactions

Test-Guided Bug Detector

  • Analyzes failing tests to detect functional bugs in code
  • Examines execution behavior, assertions, and stack traces
  • Identifies suspicious code regions causing test failures

Behavioral Mutation Analyzer

  • Systematically analyzes surviving mutants from mutation testing
  • Identifies test suite weaknesses and generates improvements
  • Categorizes why mutants survived and suggests test enhancements

Metamorphic Property Extractor

  • Automatically identifies metamorphic properties from programs
  • Enables metamorphic testing without explicit test oracles
  • Discovers input-output relationships for test generation

Metamorphic Test Generator

  • Generates test cases using metamorphic testing principles
  • Applies transformations based on metamorphic properties
  • Expands test suites and detects bugs through input-output relationships

Counterexample to Test Generator

  • Converts formal verification counterexamples into executable test cases
  • Transforms model checker outputs into unit or integration tests
  • Bridges formal verification and testing workflows

Mutation Test Suite Optimizer

  • Optimizes test suites using mutation testing analysis
  • Selects minimal subset of tests maximizing mutation kill rate
  • Reduces execution time and eliminates redundancy

Test Deduplicator

  • Analyzes test suites to identify redundant or duplicate tests
  • Examines code coverage, semantic similarity, and execution behavior
  • Groups equivalent tests and explains deduplication rationale

Java API Consistency Validator

  • Validates API consistency between two versions of Java libraries
  • Compares signatures, behavior, and exceptions
  • Identifies breaking changes and incompatible modifications

Python API Consistency Validator

  • Validates API consistency between two versions of Python libraries
  • Compares signatures, behavior, and exceptions
  • Identifies breaking changes and provides migration guidance

Code Quality & Analysis

Code Review Assistant

  • Performs automated code reviews
  • Identifies issues and suggests improvements
  • Checks coding standards compliance

Code Smell Detector

  • Detects code smells and anti-patterns
  • Suggests refactoring opportunities
  • Categorizes smells by severity

Design Smell Detector

  • Identifies architectural and design issues
  • Detects violations of design principles
  • Suggests design improvements

Code Optimizer

  • Optimizes code for performance
  • Identifies bottlenecks
  • Suggests algorithmic improvements

Dead Code Eliminator

  • Identifies unused code
  • Safely removes dead code
  • Reports elimination opportunities

Technical Debt Analyzer

  • Identifies technical debt
  • Quantifies debt impact
  • Prioritizes debt reduction

Code Pattern Extractor

  • Analyzes codebases to identify reusable code patterns and duplications
  • Generates pattern catalogs with refactoring suggestions
  • Creates reusable template code for high-value patterns

Code Search Assistant

  • Searches repositories for code related to given snippets
  • Ranks results by call chain, textual, and functional similarity
  • Outputs ranked file lists with matching code snippets

Component Boundary Identifier

  • Identifies module/component boundaries
  • Detects boundary violations
  • Analyzes architectural separation

Code Summarizer

  • Generates concise summaries of source code at multiple scales
  • Explains code functionality from functions to entire codebases
  • Helps understand complex code structures quickly

Static Bug Detector

  • Analyzes source code statically to detect potential functional bugs
  • Identifies null dereferences, incorrect conditions, unreachable code
  • Detects logic errors, resource leaks, and inconsistent state updates

Static Vulnerability Detector

  • Statically analyzes code to detect security vulnerabilities
  • Identifies buffer overflows, injection risks, insecure deserialization
  • Detects improper authentication and unsafe cryptographic usage

Vulnerability Pattern Matcher

  • Detects security vulnerabilities by matching known patterns
  • Identifies insecure coding idioms and CVE-style patterns
  • Explains why patterns are risky and conditions for exploitation

Vulnerability Root Cause Analyzer

  • Analyzes vulnerable code to identify underlying root causes
  • Identifies violated assumptions, incorrect invariants, missing validation
  • Detects unsafe component interactions

Exploitability Analyzer

  • Assesses realistic exploitability of detected vulnerabilities
  • Examines control flow, input sources, and sanitization logic
  • Determines if vulnerabilities are practically exploitable

Security Patch Advisor

  • Proposes secure remediation strategies for security vulnerabilities
  • Addresses buffer overflows, injection risks, insecure deserialization
  • Provides fixes for improper authentication and unsafe cryptographic usage

CVE Reachability Analyzer

  • Analyzes whether CVE vulnerabilities in dependencies are reachable from application code
  • Performs static and dynamic reachability analysis
  • Prioritizes CVE remediation based on actual exploitability

CVE Watchlist Action Recommendation Generator

  • Generates actionable recommendations for CVEs in dependency watchlists
  • Prioritizes CVEs based on severity, exploitability, and impact
  • Suggests patching, mitigation, or monitoring strategies

Time-Aware Dependency CVE Scanner

  • Scans dependencies for CVEs with temporal context awareness
  • Tracks CVE disclosure timelines and patch availability
  • Provides time-sensitive vulnerability management recommendations

Semantic Bug Detector

  • Detects semantic-level bugs by analyzing code behavior vs. intent
  • Infers intended purpose from names, comments, and documentation
  • Identifies mismatches between implementation and expected behavior

Behavior Preservation Checker

  • Validates that migrated or refactored codebase preserves original behavior
  • Compares runtime behavior, test results, and execution traces
  • Identifies behavioral divergences between code versions

Semantic Equivalence Verifier

  • Analyzes semantic equivalence between two code artifacts
  • Compares control flow, data flow, and observable behavior
  • Provides rigorous equivalence analysis for functions, classes, or modules

Multi-Version Behavior Comparator

  • Compares behavior across multiple versions of programs
  • Identifies functional changes, regressions, and behavioral divergences
  • Guides safe upgrades and validation processes

Regression Consistency Checker

  • Checks whether new version preserves behavior observed by tests on old version
  • Validates behavioral consistency across versions
  • Identifies unexpected behavioral changes

Interval Difference Analyzer

  • Analyzes differences in program intervals (variable value ranges) between versions
  • Detects behavioral changes and identifies potential bugs
  • Guides testing efforts based on interval analysis

Interval Profiling Performance Analyzer

  • Profiles programs to identify performance bottlenecks
  • Generates optimization recommendations with visualizations
  • Uses interval analysis for performance insights

Modular Code Enforcement (Inspired by oh-my-opencode)

  • Enforces strict modular architecture with SRP and 200 LOC limits
  • Bans catch-all files (utils.ts, helpers.ts) in favor of focused modules
  • Detects and splits files with multiple responsibilities

Dead Code Removal (Inspired by oh-my-opencode)

  • Systematic dead code removal with LSP-verified safety
  • Parallel batch processing with conflict-free execution
  • Atomic commits per batch with automatic rollback on failure

Documentation

API Documentation Generator

  • Generates API documentation
  • Creates reference documentation
  • Includes usage examples

Code Comment Generator

  • Generates inline code comments
  • Explains complex logic
  • Follows documentation standards

Markdown Document Structurer

  • Reorganizes markdown documents into well-structured format
  • Fixes heading hierarchy and generates table of contents
  • Standardizes formatting and improves readability

README Generator

  • Generates comprehensive, user-friendly README.md files
  • Includes project introduction, prerequisites, and setup instructions
  • Provides executable usage examples and repository structure overview

Change Log Generator

  • Creates change logs from commits
  • Categorizes changes by type
  • Follows semantic versioning

Code Change Summarizer

  • Generates structured pull request descriptions from code changes
  • Documents breaking changes with migration guides
  • Adds testing instructions and context enhancements

Release Notes Writer

  • Writes release notes
  • Highlights new features and fixes
  • Targets end users

Legacy Code Summarizer

  • Summarizes legacy codebases
  • Explains code functionality
  • Aids in understanding old code

Python Repository Quick Start

  • Quickly analyzes Python repositories
  • Identifies project type, entry points, and dependencies
  • Generates setup and execution instructions

Error Explanation Generator

  • Explains error messages
  • Provides context and solutions
  • Helps with debugging

Init Deep (Inspired by oh-my-opencode)

  • Generates hierarchical AGENTS.md context files throughout a project tree
  • Provides AI agents with directory-specific knowledge automatically
  • Supports max-depth control and incremental generation

Session Handoff (Inspired by oh-my-opencode)

  • Creates structured context summaries for cross-session continuation
  • Captures completed work, remaining tasks, key files, and gotchas
  • Enables seamless handoff between AI sessions or teammates

Architecture & Design

API Design Assistant

  • Assists in API design
  • Suggests RESTful patterns
  • Validates API consistency

Design Pattern Suggestor

  • Suggests appropriate design patterns
  • Explains pattern applicability
  • Provides implementation guidance

Configuration Generator

  • Generates configuration files
  • Supports multiple formats (YAML, JSON, XML)
  • Validates configuration schemas

Dependency Resolver

  • Resolves dependency conflicts
  • Suggests compatible versions
  • Analyzes dependency trees

Requirements & Specifications

Requirement Summarizer

  • Summarizes requirements documents
  • Extracts key requirements
  • Organizes by priority

Requirement Coverage Checker

  • Checks requirement coverage
  • Identifies gaps in implementation
  • Traces requirements to code and test

Requirement Comparison Reporter

  • Compares old and new requirement documents
  • Maps requirement changes to code components
  • Generates detailed modification plans in Markdown format

Ambiguity Detector

  • Detects ambiguous requirements
  • Highlights unclear specifications
  • Suggests clarifications

Scenario Generator

  • Generates usage scenarios
  • Creates user stories
  • Develops test scenarios

Specification Generator

  • Generates formal specifications
  • Converts natural language to specs
  • Validates specification completeness

Natural Language to Constraints

  • Converts NL requirements to formal constraints
  • Supports constraint languages
  • Validates constraint consistency

Strategic Planner (Inspired by oh-my-opencode)

  • Interview-based strategic planning for complex software tasks
  • Conducts gap analysis to catch hidden intentions and ambiguities
  • Generates detailed work plans with acceptance criteria and test strategy

DevOps & Deployment

Build/CI Migration Assistant

  • Migrates build systems and CI/CD configurations

CD Pipeline Generator

  • Creates CD pipeline configurations for automated deployment
  • Supports AWS, GCP, and Azure cloud platforms
  • Includes environment separation, approval gates, and rollback capabilities

CI Pipeline Synthesizer

  • Generates CI pipeline configurations for automated building and testing
  • Supports GitHub Actions with dependency caching and matrix testing
  • Includes templates for Node.js, Python, Go, and Rust projects

Config Consistency Checker

  • Detects configuration inconsistencies across environments

Containerization Assistant

  • Creates Dockerfiles and container configs
  • Optimizes container images
  • Supports multi-stage builds

Environment Setup Assistant

  • Generates environment setup scripts
  • Manages dependencies and configurations
  • Supports multiple platforms

Rollback Strategy Advisor

  • Suggests rollback strategies
  • Plans deployment reversions
  • Minimizes downtime

Docker Hub Automation

  • Automates Docker Hub tasks via Rube MCP (Composio)
  • Manages repositories, images, tags, and container registry
  • Supports Docker Hub operations

Code Instrumentation Generator

  • Automatically instruments source code to collect runtime information
  • Preserves program semantics while adding instrumentation
  • Supports various instrumentation strategies for debugging and analysis

Security-Sensitive Path Instrumenter

  • Adds structured logging instrumentation to security-critical code paths
  • Monitors authentication, authorization, input validation, and session management
  • Enables runtime monitoring of security-relevant events

Taint Instrumentation Assistant

  • Instruments code to track untrusted and sensitive data flow
  • Detects security vulnerabilities through taint analysis
  • Identifies potential injection points and data leaks

Critical Interval Security Checker

  • Analyzes code to identify security-critical time intervals
  • Detects timing vulnerabilities that could compromise security
  • Identifies race conditions and time-of-check-time-of-use issues

Release Change Analyzer (Inspired by oh-my-opencode)

  • Compares HEAD with latest published version to analyze real changes
  • Groups changes by type (feat/fix/refactor) with actual diff descriptions
  • Recommends version bump (major/minor/patch) with reasoning

Debugging & Error Handling

Bug Localization

  • Localizes bugs in code
  • Analyzes stack traces and logs
  • Suggests likely bug locations

Bug to Patch Generator

  • Generates patches for identified bugs
  • Creates minimal fixes
  • Includes test cases for fixes

Conflict Analyzer

  • Analyzes merge conflicts
  • Suggests conflict resolutions
  • Explains conflicting changes

Failure-Oriented Instrumentation

  • Selectively instruments code to capture runtime data for debugging

Git Bisect Assistant

  • Automates git bisect to find the first bad commit

Regression Root Cause Analyzer

  • Analyzes regression failures
  • Identifies root causes
  • Suggests fixes

Replay-Oriented Instrumentation

  • Records execution for deterministic replay debugging

Runtime Error Explainer

  • Explains runtime errors
  • Provides debugging guidance
  • Suggests fixes

Issue Report Generator

  • Automatically generates clear, actionable issue reports from failing tests
  • Analyzes test failures to understand expected vs. actual behavior
  • Identifies affected code components and suggests fixes

Bug History Summarizer

  • Traces and summarizes the complete lifecycle of a bug across code versions
  • Provides historical context for bug evolution
  • Helps understand bug patterns and resolution strategies

Bisect-Aware Instrumentation

  • Instruments code to support efficient git bisect operations
  • Produces deterministic pass/fail signals and concise runtime summaries
  • Creates robust test scripts for bisect workflows

Reproduction Trace Instrumenter

  • Instruments source code to capture detailed execution traces for bug reproduction
  • Records function calls, variable values, control flow, and program state
  • Generates replay scripts for deterministic bug reproduction

State Snapshot Instrumenter

  • Instruments programs to capture snapshots of key program states at runtime
  • Includes variable values, memory state, call stacks, and execution context
  • Saves snapshots in structured JSON format for analysis

Trace Collection Assistant

  • Collects, normalizes, and structures execution traces from instrumented programs
  • Processes strace, ltrace, and custom trace formats
  • Makes traces suitable for debugging, reproduction, or performance analysis

SZZ Bug Identifier

  • Performs SZZ algorithm analysis to identify bug-introducing commits
  • Traces modified lines back through version history
  • Links bug fixes to their originating changes

Semantic SZZ Analyzer

  • Extends traditional SZZ algorithm with semantic analysis
  • Distinguishes actual bug-introducing changes from refactoring
  • Provides more accurate identification of bug origins

Formal Methods & Verification

ACSL Annotation Assistant

  • Assists with ACSL annotations
  • Generates function contracts
  • Validates annotation correctness

Assertion Synthesizer

  • Synthesizes program assertions
  • Generates invariants and pre/post-conditions
  • Validates assertion correctness

Invariant Inference

  • Infers loop and program invariants
  • Uses static and dynamic analysis
  • Validates inferred invariants

Static Reasoning Verifier

  • Verifies code using static analysis
  • Checks correctness properties
  • Reports verification results

Symbolic Execution Assistant

  • Assists with symbolic execution
  • Generates path constraints
  • Explores execution paths

Counterexample Generator

  • Generates counterexamples for failed proofs
  • Creates test cases from counterexamples
  • Helps understand verification failures

Counterexample Explainer

  • Explains counterexamples
  • Provides debugging insights
  • Suggests fixes

Counterexample Debugger

  • Debugs proof failures using counterexamples from Nitpick or QuickChick
  • Identifies specification errors and missing preconditions
  • Helps resolve proof strategy issues

Abstract Domain Explorer

  • Applies abstract interpretation using different abstract domains
  • Supports intervals, octagons, polyhedra, sign, and congruence domains
  • Infers invariants, value ranges, and relationships

Abstract Invariant Generator

  • Uses abstract interpretation to infer loop invariants automatically
  • Generates function preconditions and postconditions
  • Supports formal verification workflows

Abstract State Analyzer

  • Performs abstract interpretation to infer program states
  • Analyzes variable ranges and data properties without execution
  • Reports potential runtime errors

Abstract Trace Summarizer

  • Produces summarized execution traces using abstract interpretation
  • Highlights key control flow paths and variable relationships
  • Generates high-level program behavior representations

Control Flow Abstraction Generator

  • Generates abstract Control Flow Graph (CFG) representations
  • Shows loops, branches, and function calls for static analysis
  • Supports verification and program understanding

Formal Spec Generator

  • Generates formal specifications in Isabelle/HOL or Coq
  • Converts informal requirements to formal definitions and predicates
  • Creates invariants, pre/post-conditions from natural language

C/C++ to Lean4 Translator

  • Translates C or C++ programs into equivalent Lean4 code
  • Preserves program semantics and ensures type safety
  • Generates well-typed, executable, and verifiable code

C++ to Dafny Translator

  • Translates C/C++ programs to equivalent Dafny code
  • Preserves semantics and ensures verification
  • Supports formal verification workflows

Python to Dafny Translator

  • Translates Python programs into equivalent Dafny code
  • Preserves program semantics and ensures verifiability
  • Generates well-typed, executable Dafny code

Python to Lean4 Translator

  • Translates Python programs to equivalent Lean4 code
  • Preserves semantics and ensures type safety
  • Supports formal verification in Lean4

Imperative to Coq Model Extractor

  • Extracts abstract mathematical models from imperative code
  • Supports C, C++, Python, Java for Coq formal reasoning
  • Creates Coq specifications suitable for verification

Program to Model Extractor

  • Extracts abstract mathematical models from functional code
  • Supports Haskell, OCaml, F# to Isabelle/HOL conversion
  • Enables formal reasoning about functional programs

Program Correctness Prover

  • Generates Isabelle or Coq proofs for program correctness
  • Establishes partial or total correctness from specifications
  • Uses Hoare logic and weakest precondition calculus

Proof Carrying Code Generator

  • Generates executable code with formal correctness proofs
  • Certifies safety and correctness properties in Isabelle/HOL or Coq
  • Supports verified software and safety-critical systems

Proof Skeleton Generator

  • Generates structured proof skeletons with tactics and strategies
  • Creates intermediate lemmas for theorems in Isabelle/HOL or Coq
  • Provides proof outlines for complex theorems

Proof Trace Summarizer

  • Summarizes long Isabelle or Coq proof scripts
  • Extracts high-level logical steps and reasoning flow
  • Documents proof strategies for understanding

Proof Failure Explainer

  • Analyzes and explains why Isabelle or Coq proofs fail
  • Identifies type mismatches, missing assumptions, incorrect goals
  • Detects unification failures and inapplicable tactics

Proof Refactoring Assistant

  • Restructures Isabelle or Coq proofs for better readability
  • Enhances modularity and maintainability without changing semantics
  • Eliminates repeated patterns and improves proof structure

Lemma Discovery Assistant

  • Analyzes failed or stuck proofs to propose auxiliary lemmas
  • Helps complete proofs in Isabelle/HOL or Coq
  • Addresses unprovable subgoals and stuck proof states

Library Advisor

  • Recommends relevant Isabelle/HOL or Coq standard library resources
  • Suggests theories, lemmas, and tactics based on proof goals
  • Helps find existing library support for proofs

Tactic Suggestion Assistant

  • Analyzes proof states in Isabelle or Coq
  • Suggests applicable tactics to make progress
  • Helps choose next steps in interactive proofs

Refinement Step Generator

  • Generates systematic refinement steps from specifications to implementations
  • Works in Isabelle/HOL or Coq with correctness obligations
  • Supports formal verification through refinement

Verification Boundary Reporter

  • Analyzes formal verification artifacts (Isabelle, Coq, Dafny)
  • Identifies boundaries between verified, assumed, and unverified components
  • Produces structured reports on verification coverage

Verified Pseudocode Extractor

  • Extracts language-agnostic pseudocode from verified programs
  • Preserves verified control flow and data dependencies
  • Maintains algorithmic logic from Isabelle/HOL or Coq code

Verified Spec Code Mapper

  • Establishes traceability between formal specifications and verified code
  • Maps preconditions, postconditions, invariants to code components
  • Produces structured Markdown mapping with correctness proofs

Requirement Enhancer

  • Iteratively enhances user requirements into clear specifications
  • Analyzes and clarifies incomplete or ambiguous requirements
  • Produces actionable, complete specifications

Interface Contract Verifier

  • Verifies that formal contracts (preconditions, postconditions, invariants) are preserved
  • Validates contract compliance when updating to new program versions
  • Ensures interface specifications remain consistent

Code Completion Semantic Constraints

  • Completes partial code snippets while satisfying semantic constraints
  • Produces compilable code with verification tests
  • Explains how each constraint was satisfied

Model-Guided Code Repair

  • Automatically repairs code violations of temporal properties using counterexamples
  • Reasons about model-level causes and proposes minimal fixes
  • Validates repairs through re-verification or test generation

TLA+ Guided Code Repair

  • Repairs code based on TLA+ specification violations
  • Uses TLA+ model checking results to guide repair strategies
  • Ensures repaired code satisfies temporal properties

Program to TLA+ Spec Generator

  • Automatically generates TLA+ specifications from program code
  • Identifies state variables, actions, and invariants
  • Creates formal models for verification

TLA+ Spec Generator

  • Generates TLA+ specifications from requirements or designs
  • Creates formal specifications with proper syntax
  • Supports concurrent and distributed system modeling

Requirement to TLA+ Property Generator

  • Converts natural language requirements to TLA+ temporal properties
  • Formalizes safety and liveness properties
  • Generates verifiable specifications from informal descriptions

Specification to Temporal Logic Generator

  • Translates specifications into temporal logic formulas (LTL, CTL)
  • Supports multiple temporal logic notations
  • Enables formal verification of system properties

TLA+ Model Reduction

  • Reduces TLA+ model complexity while preserving properties
  • Applies abstraction and symmetry reduction techniques
  • Improves model checking performance

SMV Model Extractor

  • Extracts SMV models from program code or specifications
  • Generates models suitable for symbolic model checking
  • Supports NuSMV and nuXmv verification tools

RTL Specification Consistency Checker

  • Checks behavioral consistency between RTL and specifications
  • Identifies satisfied, violated, underspecified, and uncheckable requirements
  • Provides detailed violation reports with execution traces

RTL Equivalence Checker

  • Verifies equivalence between two RTL implementations
  • Detects functional differences in hardware designs
  • Supports formal equivalence checking workflows

RTL Property Inference

  • Automatically infers temporal properties from RTL code
  • Discovers invariants and protocol properties
  • Generates assertions for hardware verification

Maintenance & Refactoring

Code Refactoring Assistant

  • Suggests refactoring opportunities
  • Applies refactoring patterns
  • Ensures behavior preservation

Deprecated API Updater

  • Updates deprecated API usage
  • Suggests modern alternatives
  • Automates API migration

Code Translation

  • Translates code between languages
  • Preserves functionality
  • Adapts to target language idioms

Framework Migration Assistant

  • Automatically migrates Python web applications between frameworks
  • Transforms code, configuration, and tests while preserving functionality
  • Handles route migration and request/response patterns

Spring MVC to Boot Migrator

  • Automatically migrates Spring MVC applications to Spring Boot
  • Transforms build configuration, annotations, and XML configuration
  • Preserves existing functionality while modernizing architecture

Test-Guided Migration Assistant

  • Automatically updates codebase to new language or framework versions
  • Ensures all tests continue to pass during migration
  • Provides safe, test-driven migration path

Test-Guided Debloating

  • Removes unnecessary code from repository while preserving test-exercised behavior
  • Identifies and eliminates dead code safely
  • Maintains exactly the functionality covered by test suite

Smart Mutation Operator Generator

  • Generates customized mutation operators tailored to specific codebase
  • Maximizes mutation testing effectiveness
  • Creates domain-specific mutations for better test evaluation

Code Repair Generation Combo

  • Automatically repairs buggy code and generates comprehensive tests
  • Supports Python, Java, and C++ programs
  • Diagnoses bugs, generates fixes, and creates tests to prevent regressions

LSP Refactoring (Inspired by oh-my-opencode)

  • Intelligent refactoring using LSP tools (rename, find-references, go-to-definition)
  • AST-aware pattern matching and replacement across 25 languages
  • TDD verification workflow with automatic rollback on failure

Visualization

System Diagram Generator

  • Creates system architecture diagrams
  • Supports Mermaid, PlantUML, Graphviz
  • Generates data flow and deployment diagrams

Version Control & Collaboration

Git Master (Inspired by oh-my-opencode)

  • Atomic commit discipline with automatic style detection from repo history
  • Rebase surgeon for history rewriting, conflict resolution, and branch cleanup
  • History archaeologist using git blame, bisect, log -S for code archaeology

Project Management & Issue Tracking

GitHub Triage (Inspired by oh-my-opencode)

  • Automated GitHub issue and PR triage with parallel processing
  • Classifies issues (question/bug/feature), answers questions from codebase
  • Reviews bugfix PRs and auto-merges when all safety conditions are met

Development Tools & Builders

Playwright Automation (Inspired by oh-my-opencode)

  • Browser automation via Playwright for testing, screenshots, and scraping
  • Persistent page state with incremental script-based workflow
  • Supports accessibility snapshots, network interception, and device emulation

Agent Browser (Inspired by oh-my-opencode)

  • CLI-based browser automation with ref-based element interaction
  • Snapshot-driven workflow: discover elements, interact by ref, re-snapshot
  • Supports form filling, screenshots, PDFs, cookies, and network control

Reference Searcher (Inspired by oh-my-opencode)

  • Systematic external reference searching across docs, OSS repos, and web
  • Three-layer strategy: official docs, GitHub examples, web search
  • Synthesizes findings into actionable recommendations

UI/UX Design

Frontend UI/UX (Inspired by oh-my-opencode)

  • Designer-turned-developer approach to crafting stunning UI without mockups
  • Bold aesthetic direction with distinctive typography, color, and motion
  • Anti-pattern enforcement against generic fonts and cookie-cutter design

🔁 Skills by Stages

Stages in Software Development Lifecycle (SDLC)

📕 Requirements

💡 Software Design

⌨️ Implementation

👩🏽‍💻 Testing

✅ Verification

  • Specification & Annotation

  • Abstract Interpretation & Analysis

    • Abstract Domain Explorer – Apply abstract interpretation using different abstract domains (intervals, octagons, polyhedra, sign, congruence) to analyze program variables
    • Abstract State Analyzer – Perform abstract interpretation to infer possible program states, variable ranges, and data properties without executing the program
    • Abstract Trace Summarizer – Perform abstract interpretation to produce summarized execution traces and high-level program behavior representations
    • Control Flow Abstraction Generator – Generate abstract Control Flow Graph (CFG) representations showing loops, branches, and function calls for static analysis

  • Code Translation for Verification

    • C/C++ to Lean4 Translator – Translate C or C++ programs into equivalent Lean4 code, preserving program semantics and ensuring type safety
    • C++ to Dafny Translator – Translate C/C++ programs to equivalent Dafny code while preserving semantics and ensuring verification
    • Python to Dafny Translator – Translate Python programs into equivalent Dafny code, preserving program semantics and ensuring verifiability
    • Python to Lean4 Translator – Translate Python programs to equivalent Lean4 code while preserving semantics and ensuring type safety
    • Imperative to Coq Model Extractor – Extract abstract mathematical models from imperative code (C, C++, Python, Java) suitable for formal reasoning in Coq
    • Program to Model Extractor – Extract abstract mathematical models from functional code (Haskell, OCaml, F#) for formal reasoning in Isabelle/HOL

  • Formal Verification

  • Proof Development & Assistance

    • Proof Skeleton Generator – Generate structured proof skeletons with tactics, strategies, and intermediate lemmas for theorems in Isabelle/HOL or Coq
    • Proof Trace Summarizer – Summarize long Isabelle or Coq proof scripts into high-level logical steps and reasoning flow
    • Proof Refactoring Assistant – Restructure and improve Isabelle or Coq proofs to enhance readability, modularity, and maintainability without changing semantics
    • Lemma Discovery Assistant – Analyze failed or stuck proofs and propose auxiliary lemmas to help complete the proof in Isabelle/HOL or Coq
    • Library Advisor – Recommend relevant Isabelle/HOL or Coq standard library theories, lemmas, and tactics based on proof goals
    • Tactic Suggestion Assistant – Analyze proof states in Isabelle or Coq and suggest applicable tactics to make progress
    • Refinement Step Generator – Generate systematic refinement steps from high-level specifications to concrete implementations in Isabelle/HOL or Coq

  • Counterexample Analysis

    • Counterexample Generator – Produce counterexamples when verification fails
    • Counterexample Explainer – Explain why a counterexample violates the specification
    • Counterexample Debugger – Debug proof failures using counterexamples from Nitpick (Isabelle) or QuickChick (Coq) to identify specification errors and missing preconditions
    • Proof Failure Explainer – Analyze and explain why Isabelle or Coq proofs fail, identifying root causes such as type mismatches, missing assumptions, and incorrect goals

  • Verification Reporting & Traceability

    • Verification Boundary Reporter – Analyze formal verification artifacts (Isabelle, Coq, Dafny) and produce structured reports identifying boundaries between verified, assumed, and unverified components
    • Verified Pseudocode Extractor – Extract language-agnostic pseudocode from formally verified programs (Isabelle/HOL, Coq) while preserving verified control flow and data dependencies
    • Verified Spec Code Mapper – Establish explicit traceability between formal specifications (preconditions, postconditions, invariants) and verified code components with their correctness proofs
    • Interface Contract Verifier – Verify that formal contracts are preserved when updating to new program versions
    • Behavior Preservation Checker – Validate that migrated or refactored codebase preserves original behavior
    • Semantic Equivalence Verifier – Analyze semantic equivalence between two code artifacts
    • Regression Consistency Checker – Check whether new version preserves behavior observed by tests on old version

  • TLA+ Specification & Verification

  • Hardware Verification

  • Model Checking & Extraction

💻 Deployment

🔧 Maintenance

Usage

Each skill is packaged as a skill folder containing a SKILL.md file and other necessary scripts/references that can be loaded into Claude Code or other compatible LLM systems.

Setup a Skill

# Copy the skill folder to your skills directory
cp -r skill-folder ~/.claude/skills

You may also need to make a direction if ~/.claude/skills does not exist:

mkdir ~/.claude/skills

More details of how Claude store skills and other configurations

Using a Skill

See here "How to use".

⚡ Risk Disclosure

To prevent potential security risks that skills may pose when running locally (such as accessing SSH keys, API keys, sending data to external servers, executing arbitrary system commands, or modifying global dependencies), all skills in this project have undergone security scans via Skill-Security-Scanner. The summarized report is provided below, and the full report can be accessed at here:

📊 Risk Level Statistical Report

  • Risk distribution (Total: 174 skills scanned):

  • 🔴 CRITICAL: 16 Skills (9.2%)

    Trying to access \tmp or other system dirs, installing packages

    • framework-migration-assistant
    • vulnerability-pattern-matcher
    • code-smell-detector
    • req-to-test
    • traceability-matrix-generator
    • python-test-updater
    • requirement-enhancer
    • security-sensitive-path-instrumenter
    • critical-interval-security-checker
    • static-vulnerability-detector
    • environment-setup-assistant
    • scenario-generator
    • security-patch-advisor
    • api-documentation-generator
    • test-case-documentation
    • symbolic-execution-assistant

  • 🟠 HIGH: 5 Skills (2.9%)

    Using os.system, subprocess, eval, exec

    • containerization-assistant
    • bisect-aware-instrumentation
    • code-change-summarizer
    • configuration-generator
    • code-comment-generator

  • 🟡 MEDIUM: 9 Skills (5.2%)

    Requesting network

  • 🟢 LOW: 21 Skills (12.1%)

  • ✅ SAFE: 123 Skills (70.7%)

⚠️ Note: High false positive rate; please carefully verify. For example, if the description contains words like "password," it is considered a high-risk skill. Decide for yourself whether to use it.

For more details, please see the log.

🤝 Contributing

We welcome contributions from both:

  • Researchers (new Skills, evaluation methods)
  • Practitioners (real-world use cases, pipelines)

to:

  • Contribute new skills
  • Improving existing skills (serving as baseline, improving procedures, triggering conditions, scripts, and example codes)
  • Suggesting new skill packs (packing existing skills to suit new task scenarios)

Please read Contributing Guidelines before submitting a pull request.

Quick Contribution Steps:

  • Ensure your skill is based on a real use case
  • Check for duplicates in existing skills
  • Follow the skill structure template
  • Test your skill across platforms
  • Submit a pull request with clear documentation

🎯 Vision

Our long-term vision is to build:

A shared, open Skill layer for LLM-powered Software Engineering systems

✅ Unlike prompt collections or ad-hoc demos, each Skill in this repository is:

  • Task-grounded (solves a concrete software engineering problem)
  • Reusable (clearly specified inputs and outputs)
  • Composable (can be chained into larger workflows or pipelines)
  • Tool- and artifact-aware (operates on real code, tests, specs, configs, logs)

🧰 This repo is intended to serve as a shared skill layer for:

  • AI assistants (e.g., Claude Skills, agents)
  • Tool-augmented software engineering workflows
  • Research prototypes and empirical studies
  • Industrial automation and developer productivity tools

🎉 If you are building or studying AI Agent for software engineering, this repo is for you.

Reference

Special thanks to the following links for constructing and enhancing the skills in this repository:

Reviews (0)

No results found