Getting it into your agent
One page per mod, every tool's command on it. A separate URL per tool would split the same page into five that compete with each other.
npx skills add sjarmak/coding-agent-workflows --skill formal-methodsgit clone --depth 1 https://github.com/sjarmak/coding-agent-workflowsWrote this? Show the measurements
A badge with what this costs and how it scanned, read live from this page, so it follows the numbers instead of freezing them. Markdown for a README, HTML for a documentation site or a project page.
[](https://agentmods.dev/skills/sjarmak/coding-agent-workflows/formal-methods)<a href="https://agentmods.dev/skills/sjarmak/coding-agent-workflows/formal-methods"><img src="https://agentmods.dev/badge/skills/sjarmak/coding-agent-workflows/formal-methods/github.svg" alt="Measured on agentmods" height="20"></a>Or the 80×15 button, for a site that already has a row of RSS and ATOM ones. Only the verdict fits; the numbers stay here.
<a href="https://agentmods.dev/skills/sjarmak/coding-agent-workflows/formal-methods"><img src="https://agentmods.dev/badge/skills/sjarmak/coding-agent-workflows/formal-methods.svg" alt="Reviewed on agentmods" width="80" height="20"></a>What it costs to keep this loaded
Counted locally with the o200k_base tokenizer, which is exact for GPT models; Claude uses its own tokenizer and its counts differ. Treat this as one consistent yardstick across the catalogue rather than a bill. Prices are per million input tokens.
| Model | Per session | Once invoked |
|---|---|---|
| Fable 5.1 | $0.00045 | $0.01430 |
| Opus 5.5 | $0.00018 | $0.00572 |
| Sonnet 5.5 | $0.00009 | $0.00286 |
| Haiku 4.5 | $0.00005 | $0.00143 |
Grade A, and why
formal-methods scanned grade A with 0 findings against 26 rules in 11 categories — prompt injection, anti-refusal, data exfiltration, privilege escalation, supply chain, agent snooping, system-prompt leakage, SSRF and excessive agency — measured 28d ago.
A static scan of the body, not an audit. Every finding is printed with the line that produced it so you can judge whether it matters here. A mod is markdown that instructs an agent; that is exactly why what it instructs is worth reading.
Nothing flagged
None of the 26 patterns this scan looks for appear in this file: no shell pipes, no recursive deletes, no credential paths, no hidden text, no instruction-override or anti-refusal phrasing, no agent-config snooping. That is not a guarantee, it is the absence of the things that are checkable.
How it starts
The opening of the file, as written. The whole thing — 91 lines — stays where its author put it; the contents beside it link to each section on GitHub.
Formal Methods for Bug Finding and Verification
Establish a specific property and connect the evidence to the actual implementation. Start with one bounded subsystem. Keep ordinary tests and review; formal modeling is selective, not a prerequisite for every change.
Choose the evidence
| Question | Preferred approach | Claim supported |
|---|---|---|
| Can events interleave incorrectly? | TLA+ with TLC | Counterexample, or completed exploration of the configured finite model |
| Does pure core logic satisfy a general contract? | Lean | The stated theorem for the modeled definitions, under audited assumptions |
| Does the real API preserve invariants across actions? | Property-based state-machine testing | Tested generated sequences against implementation |
| Does production code agree with an executable model? | Differential testing | Agreement for exercised inputs; not a proof of equivalence |
Use existing repository tools and models first. Check primary documentation for the pinned tool version before introducing commands or dependencies. Missing tools, resource limits, or incomplete exploration are unresolved checks, never passes. Do not rewrite production code into Lean merely to enable an audit.
Establish the contract
Derive properties from requirements, callers, and observable behavior independently of the implementation. If the requirement is ambiguous, make the ambiguity explicit before treating a behavior as a bug.
For each property, record:
- Intended behavior and relevant source locations.
- Inputs, state, transitions, and observable outputs.
- Safety invariant or progress condition; progress needs explicit scheduling/fairness and external-response assumptions.
- Environmental assumptions, excluded behavior, and evidence required for acceptance.
Examples include at-most-once settlement, obsolete responses never overwriting current state, bounded resource accounting, and eventual cleanup after cancellation under stated scheduling assumptions. Specify whether cancellation means requested or acknowledged; these are different contracts.
What this file has done since we first saw it
Hashed on every crawl. A supply-chain change to an agent config is a question of when, not whether, so the history is kept rather than the latest state alone.
- 28d ago First seen · 91 lines · 45 tokens per session scan A e2a9e8a4066f
formal-methods is a skill published in the GitHub repository sjarmak/coding-agent-workflows (7 stars, last pushed 4d ago), licensed MIT. It adds 45 tokens to every session and 1,430 once invoked, about $0.0002 per session on Opus 5.5. A static security scan graded it A with 0 findings. No closer match exists in the catalogue, so it is treated as the original; first seen 2026-10-02.
Other skills, from other repositories
health
Audits agent config, instruction drift, hooks or MCP, and AI maintainability. Use when Claude, Codex, or Pi setup looks wrong. Not for application bugs or PR review.
hunt
Finds root cause before any fix. Use when something errors, crashes, regresses, or used to work. Not for code review or new features.
browser-trace
Capture a full DevTools-protocol trace of any browser automation — CDP firehose, screenshots, and DOM dumps — then bisect the stream into per-page searchable buckets. Use when the user wants to debug a failed run, audit network/console/DOM activity, attach a trace to an in-progress session, or feed structured per-page…
testing-blocks
Use this when you have made AEM Edge Delivery Services code changes to blocks, scripts, or styles and need to validate them before opening a pull request. Covers unit testing for utilities and logic, browser testing with Playwright, linting, and guidance on what to test and how.
qa
Read-only automated QA sweep of a deployed stardust site on AEM Edge Delivery Services — validates routing, content fidelity vs the source capture, template conformance, rendered integrity (geometry, JS errors, broken images), visual regression vs baselines, metadata/SEO/JSON-LD, link integrity, accessibility (axe)…
orca-replay
Answer questions about an earlier agent run from its recording rather than from memory, and replay or fork that run. Use when the user asks why a previous run did something, which step changed a file or broke the build, whether yesterday's failure still reproduces, or whether a different model would have got it right.