reasoning-semiformally

$npx mdskill add oaustegard/claude-skills/reasoning-semiformally

Verify code patches and locate faults across module boundaries.

  • Validates fixes by tracing execution through multiple files.
  • Detects name shadowing and scope-related regression issues.
  • Skips trivial edits like formatting or documentation changes.
  • Outputs structured checkpoints for model-specific verification.

SKILL.md

.github/skills/reasoning-semiformallyView on GitHub ↗
---
name: reasoning-semiformally
version: 0.3.0
description: Apply semi-formal certificate reasoning to code analysis — patch verification, fault localization, patch equivalence. Use when reviewing patches, hunting bugs across scopes, comparing fixes, or when code reasoning requires tracing execution across files/modules. Triggers on code review, bug localization, patch comparison, name shadowing, scope analysis, regression checking.
---

# Semi-Formal Code Reasoning

Structured certificate templates that force mandatory checkpoints before conclusions.

## Skip Conditions

Do NOT apply semi-formal reasoning when:
- The change is trivial: docs, formatting, version bumps, config changes
- The bug is locally obvious: typo, off-by-one in the same function, missing comma
- No execution paths cross scope boundaries
- The task is not code analysis (text editing, data extraction, summarization)

If any skip condition is met, proceed with standard reasoning.

## Model-Specific Instructions

**If you are Haiku-class (Haiku 4.5 or similar):**
Read `haiku.md` in this skill directory. It contains full procedural templates with worked examples.

**If you are Sonnet-class or above (Sonnet 4.6, Opus):**
Read `sonnet.md` in this skill directory. It contains compact verification checkpoints.

## Composing Tasks

For complex tasks, apply templates sequentially:
1. **Fault localization** to find the bug
2. **Patch verification** to validate a proposed fix
3. **Patch equivalence** to compare alternative fixes

Each output feeds the next as premises.

More from oaustegard/claude-skills

SkillDescription
accessing-github-reposGitHub repository access in containerized environments using REST API and credential detection. Use when git clone fails, or when accessing private repos/writing files via API.
api-credentialsSecurely manages API credentials for multiple providers (Anthropic Claude, Google Gemini, GitHub). Use when skills need to access stored API keys for external service invocations.
asking-questionsGuidance for asking clarifying questions when user requests are ambiguous, have multiple valid approaches, or require critical decisions. Use when implementation choices exist that could significantly affect outcomes.
browsing-blueskyBrowse Bluesky content via API and firehose - search posts, fetch user activity, sample trending topics, read feeds and lists, analyze and categorize accounts. Supports authenticated access for personalized feeds. Use for Bluesky research, user monitoring, trend analysis, feed reading, firehose sampling, account categorization.
building-github-indexGenerate progressive disclosure indexes for GitHub repositories to use as Claude project knowledge. Use when setting up projects referencing external documentation, creating searchable indexes of technical blogs or knowledge bases, combining multiple repos into one index, or when user mentions "index", "github repo", "project knowledge", or "documentation reference".
categorizing-bsky-accountsAnalyze and categorize Bluesky accounts by topic using keyword extraction. Use when users mention Bluesky account analysis, following/follower lists, topic discovery, account curation, or network analysis.
chartingSelect the right Python charting library (seaborn, matplotlib, graphviz) and produce publication-quality static visualizations. Use when creating charts, plots, graphs, diagrams, heatmaps, visualizations from data, or when choosing between matplotlib/seaborn/graphviz. Also triggers for network diagrams, flowcharts, dependency trees, state machines, and entity-relationship diagrams. For interactive browser-rendered charts or uploaded data exploration, defer to charting-vega-lite instead.
charting-vega-liteCreate interactive data visualizations using Vega-Lite declarative JSON grammar. Supports 20+ chart types (bar, line, scatter, histogram, boxplot, grouped/stacked variations, etc.) via templates and programmatic builders. Use when users upload data for charting, request specific chart types, or mention visualizations. Produces portable JSON specs with inline data islands that work in Claude artifacts and can be adapted for production.
check-toolsValidates development tool installations across Python, Node.js, Java, Go, Rust, C/C++, Git, and system utilities. Use when verifying environments or troubleshooting dependencies.
cloning-projectExports project instructions and knowledge files from the current Claude project. Use when users want to clone, copy, backup, or export a project's configuration and files.