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 ArabelaTso/Skills-4-SE --skill formal-spec-generatorgit clone --depth 1 https://github.com/ArabelaTso/Skills-4-SEWrote 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/arabelatso/skills-4-se/formal-spec-generator)<a href="https://agentmods.dev/skills/arabelatso/skills-4-se/formal-spec-generator"><img src="https://agentmods.dev/badge/skills/arabelatso/skills-4-se/formal-spec-generator/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/arabelatso/skills-4-se/formal-spec-generator"><img src="https://agentmods.dev/badge/skills/arabelatso/skills-4-se/formal-spec-generator.svg" alt="Reviewed on agentmods" width="80" height="20"></a>- NVIDIA SkillSpector pass
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.00119 | $0.01281 |
| Opus 5 | $0.00060 | $0.00641 |
| Sonnet 5 | $0.00024 | $0.00256 |
| Haiku 4.5 | $0.00012 | $0.00128 |
Grade A, and why
formal-spec-generator 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 9d 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 — 172 lines — stays where its author put it; the contents beside it link to each section on GitHub.
Formal Specification Generator
Generate formal specifications in Isabelle/HOL or Coq from informal descriptions, source code, or mathematical statements.
Workflow
1. Understand the Input
Identify what type of input is provided:
- Informal requirements: Natural language descriptions (e.g., "a function that sorts a list")
- Source code: Existing implementations in Python, C, Java, or other languages
- Pseudocode: Algorithmic descriptions with semi-formal structure
- Mathematical definitions: Properties or theorems to formalize
2. Choose Target System
Ask the user which formal proof assistant to target:
- Isabelle/HOL: Preferred for higher-order logic, functional programming style
- Coq: Preferred for constructive logic, dependent types, proof automation
- Both: Generate specifications in both systems when requested
If not specified, default to generating both versions.
3. Identify Specification Components
Determine what needs to be formalized:
- Function definitions: Type signatures and implementations
- Data types: Algebraic data types, records, or inductive types
- Predicates: Properties and logical relationships
- Pre/post-conditions: Function contracts and correctness specifications
- Invariants: Loop invariants or data structure invariants
4. Generate Formal Specifications
Use the reference files for syntax and patterns:
- Isabelle patterns: See isabelle_patterns.md
- Coq patterns: See coq_patterns.md
- Complete examples: See examples.md
Generate specifications that include:
- Type definitions for data structures
- Function definitions with proper types
- Predicates describing properties
- Correctness specifications relating inputs to outputs
- Theorem statements (proofs can be left as
sorryin Isabelle orAdmittedin Coq)
5. Structure the Output
Organize the generated specifications clearly:
What ships with it
3 files beside SKILL.md in the same directory: the scripts, references and assets a skill reads on demand. Not counted in the per-session cost; read them before you install if any of them is executable.
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.
- 9d ago First seen · 172 lines · 119 tokens per session scan A 4273f85a6897
formal-spec-generator is a skill published in the GitHub repository ArabelaTso/Skills-4-SE (252 stars, last pushed 22d ago), licensed Apache-2.0. It adds 119 tokens to every session and 1,281 once invoked, about $0.0006 per session on Opus 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-09-03.
Other skills, from other repositories
understand-explain
Use when you need a deep-dive explanation of a specific file, function, or module in the codebase.
eli5
WHAT: Explains a codebase, a folder, a feature, a command or a pull request to someone who knows nothing about it, as a PR Lens canvas whose walkthrough builds the picture one part at a time. WHEN: /eli5 , or asked to explain code simply, for a beginner, a new hire, a non-engineer, or 'like I'm five'. KEYWORDS: eli5…
master-debate
A skill for running an adversarial, multi-round debate between two Buddhist teachers. It is designed for questions where the teachers argue from different positions.
master-milarepa
A reference skill for answering questions about Milarepa, a Tibetan Buddhist teacher associated with the Kagyu tradition. It covers retreat, hardship, Mahamudra, inner heat practices, and devotion to a teacher.
learning-and-development
Builds capability — skills gaps, career frameworks, training that transfers to the job, and internal mobility. Use this to design a career ladder, close a capability gap, decide whether to build or hire a skill, structure onboarding into a role, or work out why training keeps failing to change anything.
team-onboarding-playbook
Design a structured onboarding experience that gets new team members productive in 30, 60, and 90 days. Use when a new hire is joining, when contractors or agency partners need to ramp up, when an existing team is restructuring and members are switching focus, or when current onboarding feels chaotic and slow. Also…