general-secure-coding-agent-skills

Produces a structured summary of a requirements document — the key obligations, grouped by actor and concern, with the MUST/SHOULD/MAY breakdown. Use when onboarding to a large spec, when deciding what to implement first, or when the user asks what a 200-page standard actually requires.

Uses a model checker's counterexample trace to localize the fault in the model, propose a fix, and propagate that fix back to the source code. Use when a model checker (TLC, NuSMV, Spin) finds a violation and you need to turn the trace into a code change, not just understand it.

Alias for requirement-summarizer. Produces a structured summary of a requirements document — the key obligations, grouped by actor and concern, with the MUST/SHOULD/MAY breakdown. Use when onboarding to a large spec, when deciding what to implement first, or when the user asks what a standard actually requires.

Generates abstract invariants using domain abstraction — intervals, octagons, polyhedra, sign domains — to find invariants that concrete reasoning misses. Use when standard invariant inference fails, when the invariant involves relationships between multiple variables, or when verifying numerical code.

Dispatch skill — routes a formal specification request to the right concrete generator based on what's being specified and what needs to be proven. Use when the user asks to formally specify something without naming a target formalism, or when unsure which verification tool fits the problem.

Checks whether an implementation covers a set of requirements by tracing each requirement to code, tests, or both — and flagging gaps where a requirement has no evidence of implementation. Use when auditing for compliance, when answering "is this spec implemented", or before claiming a standard is supported.

Optimizes code for performance by identifying the actual bottleneck, choosing the right optimization lever, and measuring the result. Use when a specific operation is too slow, when a profiler has pointed at a hot path, or when the user asks to make something faster.

Translates pseudocode into idiomatic Java, inferring types, choosing collection classes, and handling exceptions per Java conventions. Use when implementing an algorithm from a paper or spec, when the user hands you pseudocode and wants Java, or when realizing a verified-pseudocode artifact.

Extracts language-agnostic pseudocode from real code, stripping syntax noise and language-specific machinery while preserving the algorithmic structure. Use when documenting an algorithm for a paper or spec, when porting and wanting a neutral intermediate, or when explaining code to someone who doesn't know the source language.

Translates C++ functions into Dafny for formal verification, modeling pointers, fixed-width integers, and manual memory as Dafny heap objects and bitvectors. Use when verifying a C++ algorithm, when proving absence of overflow or out-of-bounds access, or when building a verified reference for safety-critical C++ code.

Identifies code smells — structural patterns that correlate with maintainability problems — and explains why each matters in context. Use when reviewing a PR for structural quality, when the user asks what's wrong with a piece of code that isn't buggy, or when prioritizing refactoring targets.

TLA+-specific instance of model-guided repair — reads a TLC error trace, identifies the enabling condition that should have been false, strengthens the corresponding action, and maps the fix to source code. Use when TLC reports an invariant violation or deadlock and you have the code-to-TLA+ mapping from extraction.

Translates Python functions into Dafny, adding types, pre/postconditions, and loop invariants sufficient for Dafny to verify. Use when formally verifying a Python algorithm, when the user wants machine-checked correctness for a critical function, or when building a verified reference implementation.

Converts a model checker counterexample trace into an executable test case in the source language, so the bug found in the model is reproducible (and regression-guarded) in the real code. Use when TLC/NuSMV/Spin finds a violation and you want a failing test before writing the fix.

Finds and safely removes code that is never executed — unreachable branches, uncalled functions, unused classes, dead feature flags. Use when cleaning up after a feature removal, when the user suspects the codebase has accumulated cruft, or when reducing build/bundle size.

Creates minimal, reproducible test cases from bug reports to confirm the defect before and after a fix. Use when a bug is reported without a failing test, when the user needs a regression test for a fix, or when the user asks to reproduce a bug as a test.

Recommends the specific code change to remediate a detected vulnerability by dispatching on CWE to the matching Project CodeGuard rule's prescribed fix pattern. Use after a finding has been confirmed and located, when the user asks how to fix a vulnerability, or when generating remediation PRs.

Generates domain-specific mutation operators beyond the standard arithmetic/relational set — mutations tailored to your codebase's idioms, APIs, and bug history that standard tools don't try. Use when generic mutation testing plateaus, when your domain has specific failure modes, or when mining bug history reveals patterns standard operators miss.

Generates code comments that explain non-obvious intent, constraints, and tradeoffs — not what the code already says. Use when code is correct but opaque, when documenting for future maintainers, or when a function's why is harder to see than its what.

Sets up taint tracking by defining sources, sinks, and sanitizers from Project CodeGuard's input-validation taxonomy, then configures the target tool (CodeQL, Semgrep, custom instrumentation). Use when wiring taint analysis into CI, when the user asks for taint tracking, or when you need a source/sink catalog for a specific language.

Uses mutation testing to find weak assertions and missing tests — injects small bugs and checks if the suite catches them, then generates tests targeting the surviving mutants. Use when coverage is high but bugs still ship, when auditing test quality, or when deciding if the suite is good enough.

Diagnoses and resolves package dependency conflicts — version mismatches, diamond dependencies, cycles — across npm, pip, Maven, Cargo, and similar ecosystems. Use when install fails with a resolution error, when two packages require incompatible versions of a third, or when upgrading one dependency breaks another.

Pinpoints the exact file, function, or line in a codebase responsible for a reported bug using static and dynamic analysis signals. Use when a bug is reported but the fault location is unknown, when narrowing down a failure to a specific code region, when triaging an issue tracker ticket, or when the user asks to locate where a bug originates.

Finds and removes redundant tests — tests that cover the same code, kill the same mutants, or assert the same behavior — to shrink suite runtime without losing coverage. Use when the test suite is slow, when tests have accumulated over years of copy-paste, or when CI costs are too high.

Extracts human-readable pseudocode from a verified formal artifact (Dafny, Lean, TLA+) while preserving the verified properties as annotations, so the proof-carrying logic can be reimplemented in a production language. Use when porting verified code to an unverified target, when documenting what a formal spec actually does, or when handing a verified algorithm to an implementer.