Skills-4-SE

Applies abstract interpretation using different abstract domains (intervals, octagons, polyhedra, sign, congruence) to statically analyze program variables and infer invariants, value ranges, and relationships. Use when analyzing program properties, inferring loop invariants, detecting potential errors, or understanding variable relationships through static analysis.

Uses abstract interpretation to automatically infer loop invariants, function preconditions, and postconditions for formal verification. Generates invariants that capture program behavior and support correctness proofs in Dafny, Isabelle, Coq, and other verification systems. Use when adding formal specifications to code, generating verification conditions, inferring contracts for functions, or discovering loop invariants for proofs.

Performs abstract interpretation over source code to infer possible program states, variable ranges, and data properties without executing the program. Reports potential runtime errors including out-of-bounds accesses, null dereferences, type inconsistencies, division by zero, and integer overflows. Use when analyzing code for potential runtime errors, performing static analysis, checking safety properties, or verifying program behavior without execution.

Performs abstract interpretation to produce summarized execution traces and high-level program behavior representations. Highlights key control flow paths, variable relationships, loop invariants, function summaries, and potential runtime states using abstract domains (intervals, signs, nullness, etc.). Use when analyzing program behavior, understanding execution paths, computing loop invariants, tracking variable ranges, detecting potential runtime errors, or generating program summaries without concrete execution.

Create ACSL (ANSI/ISO C Specification Language) formal annotations for C/C++ programs. Use this skill when working with formal verification, adding function contracts (requires/ensures), loop invariants, assertions, memory safety annotations, or any ACSL specifications. Supports Frama-C verification and generates comprehensive formal specifications for C/C++ code.

CLI-based browser automation with persistent page state using ref-based element interaction. Use when users ask to navigate websites, interact with web pages, fill forms, take screenshots, test web applications, or extract information from web pages.

Detects and analyzes ambiguous language in software requirements and user stories. Use when reviewing requirements documents, user stories, specifications, or any software requirement text to identify vague quantifiers, unclear scope, undefined terms, missing edge cases, subjective language, and incomplete specifications. Provides detailed analysis with clarifying questions and suggested improvements.

Design and review APIs with suggestions for endpoints, parameters, return types, and best practices. Use when designing new APIs from requirements, reviewing existing API designs, generating API documentation, or getting implementation guidance. Supports REST APIs with focus on endpoint structure, request/response schemas, authentication, pagination, filtering, versioning, and OpenAPI specifications. Triggers when users ask to design, review, document, or improve APIs.

Generate comprehensive API documentation from repository sources including OpenAPI specs, code comments, docstrings, and existing documentation. Use when documenting APIs, creating API reference guides, or summarizing API functionality from codebases. Extracts endpoint details, request/response schemas, authentication methods, and generates code examples. Triggers when users ask to document APIs, generate API docs, create API reference, or summarize API endpoints from a repository.

Generate test assertions from existing code implementation. Use when the user has implementation code without tests or incomplete test coverage, and needs assertions synthesized by analyzing the code's behavior, inputs, outputs, and state changes. Supports Python (pytest/unittest), Java (JUnit/AssertJ), and JavaScript/TypeScript (Jest/Chai). Handles equality checks, collections, exceptions, and state verification.

Analyzes surviving mutants from mutation testing to identify why tests failed to detect them. Takes repository code, test suite, and mutation testing results as input. Identifies root causes including insufficient coverage, equivalent mutants, weak assertions, and missed edge cases. Automatically generates actionable test improvements and new test cases. Use when analyzing mutation testing results, improving test suite effectiveness, investigating low mutation scores, generating tests to kill surviving mutants, or enhancing test quality based on mutation analysis.

Compare runtime behavior between original and migrated repositories to detect behavioral differences, regressions, and semantic changes. Use when validating code migrations, refactorings, language ports, framework upgrades, or any transformation that should preserve behavior. Automatically compares test results, execution traces, API responses, and observable outputs between two repository versions. Provides actionable guidance for fixing deviations and ensuring behavioral equivalence.

Instrument code to support efficient git bisect by producing deterministic pass/fail signals and concise runtime summaries for each tested commit. Use when debugging regressions with git bisect, automating bisect workflows, creating bisect test scripts, handling flaky tests during bisection, or needing clear exit codes and logging for automated bisect runs. Helps identify the exact commit that introduced a bug through automated testing.

Summarizes the complete lifecycle of a bug across code versions, tracking its introduction, detection, fixing attempts, and regression history. Use when users need to: (1) Understand how a bug evolved over time, (2) Trace when and how a bug was introduced, (3) Analyze fix attempts and their effectiveness, (4) Identify regression patterns, (5) Generate bug lifecycle reports for documentation or post-mortems. Takes a repository, bug identifier, and version history as input.

Identify the precise location of bugs in source code, modules, and systems. Use this skill when debugging applications, investigating test failures, analyzing error reports, tracing runtime issues, or performing root cause analysis. Analyzes stack traces, error messages, failing tests, and code patterns to pinpoint buggy functions, classes, files, or modules with confidence rankings and supporting evidence.

Automatically generates executable tests that reproduce reported bugs from issue reports and code repositories. Use when users need to: (1) Create a test that reproduces a bug described in an issue report, (2) Generate failing tests from bug descriptions, stack traces, or error messages, (3) Validate bug reports by creating reproducible test cases, (4) Convert issue reports into executable regression tests. Takes a repository and issue report as input and produces test code that reliably triggers the reported bug.

Generate code fixes and patches from bug reports, failing test cases, error messages, and stack traces. Use this skill when debugging code, fixing test failures, addressing GitHub issues, resolving runtime errors, or patching security vulnerabilities. Analyzes the bug context, identifies root causes, and generates precise code patches with explanations and validation steps.

Automatically migrates build systems and CI/CD configurations to target platforms. Use when modernizing build infrastructure, switching CI/CD providers, or standardizing across projects. Supports common migration paths including Maven↔Gradle, npm↔Yarn, Travis CI→GitHub Actions, CircleCI→GitHub Actions, Jenkins→GitLab CI, and GitLab CI→GitHub Actions. Analyzes existing configuration, generates equivalent target configuration, maps dependencies and commands, and provides validation and migration documentation.

Translate C or C++ programs into equivalent Lean4 code, preserving program semantics and ensuring the generated code is well-typed, executable, and can run successfully. Use when the user asks to convert C/C++ code to Lean4, port C/C++ programs to Lean4, translate imperative code to functional Lean4, or create Lean4 versions of C/C++ algorithms.

Generate GitHub Actions deployment workflows for automated deployment to staging and production environments on cloud platforms (AWS, GCP, Azure). Use when setting up continuous deployment pipelines, creating deployment automation, or configuring multi-environment deployment strategies. Includes templates for environment-specific deployments with approval gates, secrets management, and rollback capabilities.