oaustegard/reasoning-semiformally
reasoning-semiformally/SKILL.md
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.
$ install --global
skillsauthnpx skillsauth add oaustegard/claude-skills reasoning-semiformallyInstall this skill globally with one command. Works with Claude Code, Cursor, and Windsurf.
Security Scan Results
3 of 9 scanners reported clean
Some scanners were skipped, did not run, or reported a non-clean status. Review each row below.
3
Scanners Passed
9
Scanners in report
Clean
TrivyContainer and dependency vulnerability scanner
95%
Clean
SemgrepStatic code analysis for vulnerabilities
95%
Clean
mcp-scan (Snyk)Model Context Protocol security validation
95%
Skipped
Snyk (dep)Open source security scanning
50%
Skipped
Socket.devSupply chain security analysis
50%
Skipped
VirusTotalMulti-engine malware detection
50%
Skipped
CrowdStrikeAdvanced threat intelligence
50%
Skipped
OSV-ScannerOpen Source Vulnerability database check
50%
Skipped
OWASP Dep-Check
50%
Last scanned: Apr 20, 2026, 6:04 AM8.4s4 files scanned
SKILL.md
- 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:
- Fault localization to find the bug
- Patch verification to validate a proposed fix
- Patch equivalence to compare alternative fixes
Each output feeds the next as premises.
Related Skills
oaustegard/verifying-claims
development
VerifiedTrustedCommunity
--- name: verifying-claims description: Check that a document's claims about code are actually true by reading the prose, the code, and the tests and reporting (or fixing) where they disagree. Use whenever the user wants to verify a README, guide, spec, or docstring still matches the code; whenever they mention documentation drift, doc-code sync, "is this still accurate", stale docs, or keeping docs/tests/code consistent; before publishing or merging a docs change; or as a periodic doc-accuracy
125SKILL.mdUpdated Jun 8, 2026
oaustegard/querying-markdown
tools
VerifiedTrustedCommunity
Query, filter, and transform Markdown structurally with mq — a jq-like CLI for Markdown. Use to extract headings/sections/code-blocks/links from .md files, build a table of contents, pull code blocks of a given language, slice or reshape LLM prompt/output Markdown, or batch-transform docs. Triggers on "extract sections from this markdown", "get all the code blocks", "jq for markdown", "mq", or any structural query over Markdown that grep/Read can't do cleanly.
125SKILL.mdUpdated Jun 8, 2026
oaustegard/composing-html
development
VerifiedTrustedCommunity
Composes single-file HTML artifacts (PR review writeups, status reports, incident postmortems, slide decks, design systems, prototypes, flowcharts, module maps, feature explainers, kanban boards, prompt tuners) from a small JSON spec instead of hand-written HTML/CSS/JS. Use when the user asks to "compare options side-by-side", requests an HTML version of a report or review or deck, asks for a flowchart, status update, postmortem, design system reference, interactive prototype, custom editor — or explicitly says "HTML artifact", "single HTML file", "self-contained HTML". Skip for ad-hoc HTML snippets (forms, emails, embedded widgets) where there's no template fit.
125SKILL.mdUpdated May 11, 2026
oaustegard/flowing
development
VerifiedTrustedCommunity
DAG workflow runner that encodes control flow in code, not prose. Use when a procedure has 3+ steps with branching, retries, or validation that must be enforced — gates as `when=`, edge contracts as `validate=`, predicate loops as `retry_until=`. The runner owns the graph; the LLM provides leaves. Also covers parallel execution, checkpoint resume, detached side-effects.
125SKILL.mdUpdated Apr 19, 2026