agentmods.dev

writing-isabelle-proofs

writing-isabelle-proofs is a skill for Claude Code, Codex from OutlineDriven/odin-claude-plugin. It costs 39 tokens per session (1,158 once invoked), scanned A, original, Apache-2.0.

A skill for writing and checking Isabelle/HOL proofs, which are machine-checked arguments written in the Isabelle proof system. It also supports Isabelle's Sledgehammer automation and AFP, a collection of reusable formal proofs.

In plain words
What is it for?
Use it to create, review, or maintain Isabelle/HOL theories, run automated proof search, or use an existing AFP entry. It is not intended for Lean 4 proofs.
Why use it?
It helps maintain formal proofs while requiring the Isabelle session to build successfully and preventing unfinished placeholders or unsupported assumptions. Changes stay in local theory and session files.

Skill for Claude CodeCodex

Written for Claude Code and Codex: shipped in a Claude Code plugin, but also agents/openai.yaml present.

Part of the odin-formal plugin — 9 skills shipped together

not rated 35repo yesterday A scan SkillSpector: pass 39 tokens original Apache-2.0

Good fit Use it to create, review, or maintain Isabelle/HOL theories, run automated proof search, or use an existing AFP entry. It is not intended for Lean 4 proofs.

Compare 6 skills from other repositories ↓
Install with agentmods
npx agentmods add skills/outlinedriven/odin-claude-plugin/writing-isabelle-proofs
View source ↗ OutlineDriven/odin-claude-plugin outlinedriven.github.io
Install

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.

Any agent
npx skills add OutlineDriven/odin-claude-plugin --skill writing-isabelle-proofs
Clone the repo
git clone --depth 1 https://github.com/OutlineDriven/odin-claude-plugin

Made for: Claude Code, Codex.

Or install odin-formal, the plugin that ships this one along with the rest of its 9 skills.

Wrote 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.

agentmods badge for writing-isabelle-proofs

README.md
[![agentmods](https://agentmods.dev/badge/skills/outlinedriven/odin-claude-plugin/writing-isabelle-proofs/github.svg)](https://agentmods.dev/skills/outlinedriven/odin-claude-plugin/writing-isabelle-proofs)
Your own site
<a href="https://agentmods.dev/skills/outlinedriven/odin-claude-plugin/writing-isabelle-proofs"><img src="https://agentmods.dev/badge/skills/outlinedriven/odin-claude-plugin/writing-isabelle-proofs/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.

agentmods 80×15 button for writing-isabelle-proofs

Your own site · 80×15
<a href="https://agentmods.dev/skills/outlinedriven/odin-claude-plugin/writing-isabelle-proofs"><img src="https://agentmods.dev/badge/skills/outlinedriven/odin-claude-plugin/writing-isabelle-proofs.svg" alt="Reviewed on agentmods" width="80" height="20"></a>
Per session 39 Skills are progressive disclosure: only the name and description are preloaded; the body loads when the skill is used.
When invoked 1,158 The whole file, excluding the scripts and references it only reads on demand.
Security scan A 0 findings. A grade says what 26 rules found in the file — not that it is safe. Third-party audits
  • NVIDIA SkillSpector pass 7 Sept 2026
How audits are shown
Origin original No closer match found in the catalogue.
Token cost

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.

ModelPer sessionOnce invoked
Fable 5.1 $0.00039 $0.01158
Opus 5 $0.00019 $0.00579
Sonnet 5 $0.00008 $0.00232
Haiku 4.5 $0.00004 $0.00116

Measured 4d ago against content hash b7def693a843, method: parsed. Prices are Anthropic first-party input rates as of 2026-09-10, from the pricing page.

Security

Grade A, and why

writing-isabelle-proofs 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 4d 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.

plugins/odin-formal/skills/writing-isabelle-proofs/SKILL.md · 38 lines

How it starts

The opening of the file, as written. The whole thing — 38 lines — stays where its author put it; the contents beside it link to each section on GitHub.

Writing Isabelle proofs

Contract

Field Bound contract
Trigger The task is to write, review, or maintain Isabelle/HOL proofs, to drive Sledgehammer against a goal, or to build on an AFP entry. Methodology stays with proof-driven.
Authority Reversible local: writes only theory files, session ROOT files, and Isabelle configuration inside the target project; rollback is version control. No remote mutation.
Side effect Local writes to .thy sources, ROOT session definitions, and the AFP checkout already on disk. No remote mutation.
Done isabelle build of the session succeeds, no sorry remains, and no axiomatization enters the delivered diff.

Inputs

  • Isabelle2025-2, made available January 2026. Install the platform bundle from isabelle.in.tum.de: Isabelle2025-2_linux.tar.gz, Isabelle2025-2_linux_arm.tar.gz, Isabelle2025-2.exe for Windows, or Isabelle2025-2_macos.tar.gz. There is no LTS, so pin the bundle version.
  • The theory sources (.thy), the session ROOT file, and for AFP work, the AFP release matching the Isabelle version.
  • Sledgehammer provers ship with the official package: CVC4, cvc5, E, SPASS, Vampire, veriT, Z3, and Zipperposition.

Procedure

  1. Open the session in the Prover IDE. Run isabelle jedit FILES to edit theories in the bundled jEdit Prover IDE, where the prover checks continuously. Define the session in a ROOT file (session Name = HOL with its theories), and extend the session search with -d DIR or a ROOTS catalog when sessions span directories. Done when: the theory holds a checked state in the IDE and isabelle build -D . finds the session.
  2. State the skeleton before proving. Write the target lemma and every helper lemma with sorry in place of a proof, then have the IDE check the skeleton: sorry is accepted in the IDE and by the batch build alike, and the build only warns, so the IDE is for iterating and the log scan is the completion check. Each sorry marks an independent work unit. Done when: every sorry is an identified work unit and the IDE checks the skeleton.
  3. Fill goals: automation first, then structure. Close routine goals with by simp or by auto. For a nontrivial goal, run sledgehammer: it drives the bundled external provers and returns a one-line proof such as by (metis ...), which is pasted into the theory. try0 runs a basket of standard methods; nitpick and quickcheck search for counterexamples. Structure what automation cannot close as Isar: proof ... qed with fix, assume, and show (thus expands to then show), with the induction and cases methods for recursive and case goals. Keep apply chains short; the manual defines apply m as backwards refinement, and long chains hide the proof state. Done when: every sorry is replaced and the build is green.
  4. Gate the result. The batch build does not fail on sorry: with the default quick_and_dirty = false it only emits a warning (the theorem is recorded as an oracle), and quick_and_dirty merely relaxes proof checking rather than gating sorry. Scan the build log for sorry and the delivered diff for sorry and axiomatization, and rebuild the session rather than trusting the IDE's incremental state. Done when: isabelle build succeeds at the defaults and the build log and delivered diff contain no sorry and no new axiomatization.
  5. Build on AFP entries. Register the extracted AFP with isabelle components -u <path-to-afp>/thys, then import an entry by its own session name, for example imports "ABC.Some_ABC_Theory". AFP sessions carry no extra namespace prefix. Done when: the AFP import resolves and the session builds.

Read the full file on GitHub · 38 lines

Files

What ships with it

1 file 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.

Changes

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.

  1. 4d ago First seen · 38 lines · 39 tokens per session scan A b7def693a843

Subscribe to this mod's changes

writing-isabelle-proofs is a skill published in the GitHub repository OutlineDriven/odin-claude-plugin (35 stars, last pushed yesterday), licensed Apache-2.0. It adds 39 tokens to every session and 1,158 once invoked, about $0.0002 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-06.

Claude Codeclaude-code-pluginclaude-code-pluginsclaude-marketplaceclaude-pluginsoutline-driven-development
Related

Other skills, from other repositories

systematic-debugging

Use when encountering any bug, test failure, or unexpected behavior, before proposing fixes.

obra/superpowers · 21 tokens

local-ai-agents

Build local-first AI agents that run entirely on a developer workstation with Microsoft Foundry Local and Qwen function-calling models. Covers Small Language Models (SLMs), the OpenAI-compatible local endpoint, sandboxed local tools, local RAG with Chroma, local MCP servers, hybrid cloud/local routing, and the…

microsoft/ai-agents-for-beginners · 200 tokens

next-cache-components-adoption

Turn on Cache Components in a Next.js app and resolve the blocking routes it surfaces. Use when the user wants to enable, adopt, or migrate to Cache Components, flip the cacheComponents flag, work through a flood of blocking-prerender / instant validation errors, run the cache-components-instant-false codemod, or…

vercel/next.js · 95 tokens

insight-error-page

Write or audit an insight-kind error page for the Next.js dev overlay. Use when creating a new errors/ .mdx page, auditing an existing one, or checking that a page matches the framework fix cards. Covers page structure, title alignment, FixCard cards with Copy prompt button, code snippets, terminology verification…

vercel/next.js · 83 tokens

next-cache-components-optimizer

Drive a Next.js route to instant navigation by setting up an agentic loop, under Cache Components / PPR, on initial load (hard navigation) and client-side navigation (soft navigation). Encode the goal as a failing @next/playwright instant() e2e and work it to green, one verified route at a time; the shipped test then…

vercel/next.js · 170 tokens

next-partial-prefetching-adoption

Turn on Partial Prefetching in a Next.js app and work through the insights it surfaces. Use when the user wants to enable or adopt Partial Prefetching, flip the partialPrefetching flag, opt routes in with export const prefetch = 'partial', audit Link prefetch={true} behavior, preserve existing prefetched UI with…

vercel/next.js · 103 tokens