Claude Skills by ArabelaTso

Generate implementation code and tests from written specifications. Use when the user provides specifications (natural language descriptions, formal specs, requirements documents, API specs) and asks Claude to implement the described functionality. Supports data structures, algorithms, classes, functions, and includes automatic test generation to validate implementation against specification.

Generate formal specifications including preconditions, postconditions, invariants, and contracts from code or requirements. Use this skill when documenting APIs, creating formal verification annotations, defining function contracts, specifying class invariants, writing design-by-contract code, or preparing code for formal verification. Supports multiple specification languages including JML, ACSL, Dafny, Eiffel contracts, and documentation annotations.

Translate natural-language requirements or structured specification documents into formal temporal logic properties (LTL, CTL, safety/liveness properties). Use when users need to formalize requirements for model checking, formal verification, or property specification. Handles embedded/real-time systems, hardware verification, concurrent systems, and reactive systems. Resolves ambiguities, asks clarifying questions when needed, and outputs machine-checkable formulas with explanations. Support...

Automatically migrate Spring MVC applications to Spring Boot. Use when you need to modernize a Spring MVC project to Spring Boot while preserving functionality. The skill analyzes the codebase, updates build configuration (Maven/Gradle), migrates annotations, converts XML configuration to Java/properties, updates controllers and tests, and creates the Spring Boot main application class. Creates git commits for each migration phase and generates a comprehensive summary. Supports both Maven and...

Instrument programs (Python, C/C++, Java) to capture snapshots of key program states at runtime, including variables, memory, and call stacks. Use when you need to debug complex issues, reproduce test cases, prepare traces for formal verification, or analyze program execution. Supports manual instrumentation points, automatic function/method instrumentation, and conditional triggers. Outputs structured JSON snapshots for debugging, replay, and verification workflows.

Analyze source code statically to detect potential functional bugs including null dereferences, incorrect condition checks, unreachable code, inconsistent state updates, logic errors, resource leaks, and type mismatches. Report suspicious code locations with detailed explanations, severity levels, and confidence assessments. Use when reviewing code for bugs, performing code audits, or when the user asks to find bugs, detect issues, analyze code for problems, or perform static analysis.

Verify code correctness statically against specifications using type checking, contract verification, and formal methods. Use when: (1) Verifying type safety and null safety in Python, Java, or C/C++ code, (2) Checking design-by-contract specifications (preconditions, postconditions, invariants), (3) Validating code against formal specifications, (4) Ensuring code quality and correctness before runtime, (5) Finding potential bugs through static analysis. Supports Python (mypy, contracts), Jav...

Statically analyze code to detect security vulnerabilities including buffer overflows, injection risks (SQL, command, XSS), insecure deserialization, improper authentication, hard-coded credentials, and unsafe cryptography. Use when: (1) Performing security code review, (2) Analyzing code for OWASP Top 10 vulnerabilities, (3) Identifying CWE-classified weaknesses, (4) Generating security audit reports, (5) Reviewing code before deployment, or (6) Assessing third-party code security. Findings ...

Interview-based strategic planning for complex software tasks. Conducts structured requirements gathering, gap analysis, and generates detailed work plans before implementation begins.

Performs symbolic execution to detect potential errors by exploring execution paths, solving path constraints, and generating test inputs. Use when you need to analyze code for bugs like null dereferences, division by zero, buffer overflows, or assertion violations. Also use to generate test inputs that exercise different code paths, find edge cases, or explore all reachable program states. Supports Python, Java, and C/C++ through manual symbolic execution techniques and integration with tool...

Creates visual representations of system structure including architecture diagrams, data flow diagrams, deployment diagrams, and sequence diagrams. Use when Claude needs to visualize system components, infrastructure, data flows, or interactions. Supports Mermaid (recommended for Markdown/GitHub), PlantUML (for detailed UML), and Graphviz/DOT (for complex networks). Trigger when users request diagrams, visualizations, or ask to "show", "diagram", "visualize", or "map out" system architecture,...

Identifies bug-introducing commits using SZZ-style analysis based on bug-fixing commits, commit history, and code blame information. Use this skill when you need to trace bugs back to their origin, identify which commits introduced bugs, analyze bug-fix commits to find root causes, perform software repository mining for bug analysis, or conduct empirical studies on software defects. Triggers when users ask to find bug-introducing commits, identify when a bug was introduced, trace bug origins,...

Analyze proof states in Isabelle or Coq and suggest applicable tactics to make progress. Use when users need help with: (1) Choosing the next tactic in an interactive proof, (2) Understanding what tactics apply to their current goal, (3) Getting unstuck in a proof, (4) Learning which tactics work for specific goal structures (conjunctions, implications, induction, etc.). Provides 3-5 ranked tactic suggestions with explanations for intermediate-level proofs in both Isabelle/Isar and Coq.

Instruments code to track the flow of untrusted or sensitive data at runtime, enabling detection of injection vulnerabilities, data leaks, and privilege violations. Use when users need to: (1) Track untrusted input propagation through code, (2) Detect SQL injection, XSS, or command injection vulnerabilities, (3) Identify sensitive data leaks, (4) Monitor privilege escalation paths, (5) Perform dynamic taint analysis for security testing. Supports Python, Java, JavaScript, and C/C++ with confi...

Detect and analyze areas with high maintenance cost, poor design, or accumulated technical debt. Use this skill when reviewing codebases for quality issues, planning refactoring efforts, conducting code audits, assessing project health, identifying maintenance hotspots, or prioritizing technical improvements. Analyzes code smells, architectural issues, dependency problems, test quality, documentation gaps, and provides actionable recommendations with priority rankings.

Generate boilerplate code and project templates/skeletons automatically. Use when: (1) Creating new projects from scratch (React app, FastAPI backend, Express API), (2) Generating repetitive code patterns (CRUD endpoints, models, controllers), (3) Scaffolding components, services, or modules, (4) Creating test boilerplate, (5) Setting up monorepo structures. Provides project templates and code generation patterns for common development tasks.

Generate comprehensive test case documentation from test code, test framework output, existing test docs, and source code context. Use when documenting test suites, creating test specifications, generating test coverage reports, onboarding developers to testing practices, or preparing QA documentation. Analyzes test functions (pytest, unittest) to extract test names, docstrings, assertions, and organization, then produces structured markdown with both overview-level summaries and detailed tes...

Automatically reduces bug-triggering test cases to minimal form while preserving the failure. Use when debugging with large, complex test cases that need simplification, reproducing bugs with minimal examples, or creating regression tests from verbose failure scenarios. Takes a failing test and systematically removes unnecessary inputs, steps, assertions, and code using delta debugging and other reduction algorithms. Supports unit tests, integration tests, input files, and multiple programmin...

Analyzes test suites to identify redundant and duplicate test cases using coverage analysis, semantic similarity, and execution results. Use this skill when you need to reduce test suite size, identify redundant tests, optimize test execution time, analyze test coverage overlap, find tests with identical behavior, or improve test suite maintainability. Triggers when users ask to deduplicate tests, find redundant test cases, reduce test suite size, identify duplicate tests, or optimize test co...

Generate implementation code that passes existing unit tests. Use when the user provides test files (Python pytest/unittest, Java JUnit/TestNG) and asks Claude to implement the code to make those tests pass. Supports full TDD workflow - analyzing tests, generating implementation, running tests, debugging failures, and iterating until all tests pass.

Analyze failing tests to detect functional bugs in code. Takes repository and failing test output as input, analyzes execution behavior, assertions, and stack traces to identify suspicious code regions and root causes. Use when debugging test failures, investigating regression bugs, or understanding why tests fail. Explains the bug mechanism, identifies affected code, and suggests fixes based on test expectations vs actual behavior.

Removes unnecessary code from a repository while preserving exactly the behavior exercised by a given test suite. Use this skill when you need to debloat, slim down, or remove unused code from a codebase based on test coverage. The skill analyzes which code elements (files, classes, functions, methods, branches, imports) are exercised by tests, identifies unreachable or unused code, and safely removes it while ensuring all tests continue to pass. Triggers when users ask to remove unused code,...

Automatically updates a codebase to a new language version, framework version, or library update while ensuring all tests still pass. Use this skill when migrating Python 2→3, upgrading framework versions (React, Django, Angular), updating dependencies, or performing any version migration where tests define correct behavior. The skill analyzes failing tests caused by migration, categorizes errors (import errors, API changes, type errors, behavior changes), proposes systematic fixes, and verif...

Generates automated test oracles to verify correct software behavior. Creates assertion-based oracles (expected values), property-based oracles (invariants), differential oracles (comparing implementations), and metamorphic oracles (input transformations). Use when you need to generate assertions for test cases, identify invariants that should always hold, compare new vs legacy implementations, create metamorphic test relationships, validate function correctness, or improve test coverage with...

Analyzes test suites and suggests optimal test execution order based on code change impact and project requirements. Use when optimizing CI/CD pipelines, deciding which tests to run before committing, or selecting critical tests under time constraints. Prioritizes tests by analyzing recently modified files, test dependencies, and coverage overlap. Outputs detailed rankings with priority scores and reasoning to help teams run the most impactful tests first.

Scan repositories for newly disclosed CVEs in dependencies after a specific cutoff date. Takes a repository path, cutoff date (YYYY-MM-DD), and optional parameters for transitive dependencies. Parses dependency manifests (package.json, pom.xml, requirements.txt, go.mod, Cargo.toml) and lockfiles to extract exact versions. Queries vulnerability databases (OSV.dev, NVD, GitHub Advisory) to identify CVEs disclosed strictly after the cutoff date. Distinguishes between newly disclosed CVEs and pre...

Automatically repair C/C++ code violations detected by TLA+ model checking. Takes a program, TLA+ specification, and TLC counterexample trace as input, then generates minimal code modifications to eliminate the violation. Use when: (1) TLC model checker reports an invariant violation, deadlock, or temporal property failure, (2) You have a counterexample trace and need to fix the corresponding code, (3) You need to understand how a TLA+ violation maps to program-level bugs, (4) You want to val...

Automatically simplify and minimize TLA+ specifications by reducing redundant state variables, merging equivalent actions, and minimizing invariants while preserving specified properties. Use when working with TLA+ specifications that need optimization, simplification, or reduction. Triggers when users ask to minimize, reduce, simplify, or optimize TLA+ specs, or when they want to remove redundancy from formal specifications while maintaining semantic equivalence.

Automatically generate TLA+ specifications from source code (C/C++, Python) for formal verification of distributed systems. Use when users need to: (1) Generate TLA+ specs from program implementations, (2) Model distributed systems, consensus protocols, or concurrent algorithms, (3) Extract state variables, actions, and invariants from code, (4) Create formal specifications for model checking with TLC, (5) Verify safety and liveness properties of distributed systems. Particularly effective fo...

Collect, normalize, and structure execution traces from instrumented programs (strace, ltrace) into JSON format for downstream analysis. Use when working with system call traces, library call traces, or execution logs that need to be analyzed for debugging, test case reproduction, or verification. Supports parsing strace/ltrace output, filtering noise, extracting debug information, and preparing traces for bug analysis or reproduction workflows.

Builds traceability matrices connecting requirements to design documents to source code implementation, tracking the complete development lifecycle. Use when you need to verify implementation completeness, ensure all requirements are implemented in code, generate compliance documentation, audit requirement coverage, identify orphaned code, or create traceability reports for stakeholders. Supports parsing requirements from Markdown, Word, and PDFs; extracting design from architecture docs and ...

Automatically generates comprehensive unit tests for functions, classes, and modules. Use when you need to create tests for Python (pytest, unittest) or Java (JUnit, TestNG) code. Generates tests with comprehensive coverage including happy paths, edge cases, and error conditions. Analyzes existing test patterns in the codebase to match style and conventions. Supports mocking, parameterized tests, fixtures, and follows best practices for each framework.

Analyze formal verification artifacts (Isabelle, Coq, Dafny, etc.) and produce structured reports identifying the precise boundary between verified, assumed, and unverified components. Use when assessing verification coverage, understanding trust boundaries, auditing formal proofs, or documenting verification scope. Reports explicitly list verified code, assumptions, axioms, trusted computing base, and unverified components. Conservative and explicit about verification status without attempti...

Extract language-agnostic pseudocode from formally verified programs (Isabelle/HOL, Coq) while preserving verified control flow, data dependencies, and algorithmic logic. Use when: (1) Users have verified code and need readable pseudocode, (2) Documenting verified algorithms for broader audiences, (3) Translating verified implementations to other languages, (4) Creating algorithm specifications from verified code, (5) Preserving verification guarantees in pseudocode form, or (6) Abstracting p...

Establish explicit traceability between formal specifications (preconditions, postconditions, invariants) and verified code components with their correctness proofs. Produce structured Markdown mapping reports showing verification coverage and proof evidence. Use when auditing formal verification, documenting verified systems, establishing traceability for certification, or when the user asks to map specifications to code, generate verification reports, or analyze verification coverage in Coq...

Detects security vulnerabilities by matching code against known vulnerability patterns, insecure coding idioms, and CVE-style patterns. Explains why patterns are risky and under what conditions they are exploitable. Use when analyzing code for security issues, reviewing for common vulnerabilities, or assessing exploitability of suspicious code patterns.

Analyze vulnerable code to identify underlying root causes such as violated assumptions, incorrect invariants, missing validation checks, or unsafe component interactions. Use when investigating security vulnerabilities, CVEs, exploit code, or security audit findings. Infers why the vulnerability exists beyond surface symptoms, identifies systemic issues, and explains the chain of failures that enable exploitation.