What is f-star-effectful-verification?

A workflow for formally checking effectful code written in F*. It uses mathematical contracts, refinement types, and an automated solver to prove that the implementation meets those contracts, then checks code extraction.

It is for verifying F* modules and interfaces, recording trusted assumptions, and checking extraction for a selected code-generation target.

It helps expose incorrect assumptions and unverified trust boundaries in security-sensitive code. The verification must pass without silently allowing unanswered solver obligations.

f-star-effectful-verification — Skill for Claude Code and Codex by Out

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 f-star-effectful-verification

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.

README.md

[![agentmods](https://agentmods.dev/badge/skills/outlinedriven/odin-claude-plugin/f-star-effectful-verification/github.svg)](https://agentmods.dev/skills/outlinedriven/odin-claude-plugin/f-star-effectful-verification)

Your own site

<a href="https://agentmods.dev/skills/outlinedriven/odin-claude-plugin/f-star-effectful-verification"><img src="https://agentmods.dev/badge/skills/outlinedriven/odin-claude-plugin/f-star-effectful-verification/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.

Your own site · 80×15

<a href="https://agentmods.dev/skills/outlinedriven/odin-claude-plugin/f-star-effectful-verification"><img src="https://agentmods.dev/badge/skills/outlinedriven/odin-claude-plugin/f-star-effectful-verification.svg" alt="Reviewed on agentmods" width="80" height="20"></a>

Per session 36 Skills are progressive disclosure: only the name and description are preloaded; the body loads when the skill is used.

When invoked 934 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.

Model	Per session	Once invoked
Fable 5.1	$0.00036	$0.00934
Opus 5	$0.00018	$0.00467
Sonnet 5	$0.00007	$0.00187
Haiku 4.5	$0.00004	$0.00093

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

Security

Grade A, and why

f-star-effectful-verification 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/f-star-effectful-verification/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.

Effectful verification in F*

Contract

Field	Bound contract
Trigger	The task is to verify effectful code with F* refinement types and the effect system, with obligations discharged to SMT, in the HACL* or Project Everest style. Methodology stays with proof-driven.
Authority	Reversible local: writes only F* source and interface files, extraction configuration, and project build files inside the target project; rollback is version control. No remote mutation.
Side effect	Local writes to `.fst` and `.fsti` files and to build or extraction configuration. No remote mutation.
Done	`fstar.exe` verifies the module with `admit_smt_queries` at its default false, the `assume val` ledger names every trust boundary, and extraction runs for the chosen codegen target.

Inputs

F* release v2026.08.30 (dated releases ship weekly), installed with opam install fstar or fetched as the dated binary release. The binary package ships bin/fstar.exe and its own Z3; a source install must supply Z3.
The module to verify, its interface (.fsti) where the contract is split from the implementation, and the extraction target.
Editor support: --ide mode, fstar-mode for Emacs, fstar-vscode-assistant for VS Code.

Procedure

Run the verifier on a trivial file. Verify with fstar.exe File.fst: each failed obligation comes back as an error at a source span, for example Sample.fst(11,26-11,31): (Error 19) Subtyping check failed, followed by the error count. Done when: a trivial module verifies with zero reported errors.
Type the fragment before proving it. Write refinements in the x:t { e } form so invalid states fail to typecheck. Mark total definitions with the default effect Tot, an abbreviation of the primitive PURE; keep specification-only computation in GHOST; give stateful code the ML effect with requires and ensures contracts on the heap. Done when: the file typechecks, every definition's effect is stated, and each effect is minimal.
Discharge obligations one at a time. Read each error span, state the missing intermediate fact as an assert or as a separate lemma, and re-run. --query_stats reports per-query SMT cost and is the first tool for a slow or failing query; scope option changes to a region with #push-options "..."/#pop-options. Done when: every reported obligation is discharged and the module verifies.
Gate against admitted queries. Keep admit_smt_queries at its default false for delivered code; a module that only verifies with it true is unproven. Each assume val is a declared trust boundary: list it with its type and the plan to prove it or audit it. Done when: the module verifies at the defaults and the assume val ledger names every trust boundary.
Extract. Extract with --codegen OCaml or --codegen FSharp, adding search paths with --include PATH. GHOST definitions stay out of extraction, so the emitted code carries only the verified computational content. Done when: extraction completes for the chosen target and the generated code matches the verified interfaces.

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.

agents/openai.yaml 220 B

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.

4d ago First seen · 38 lines · 36 tokens per session scan A ee568f8e6c4c

Subscribe to this mod's changes

f-star-effectful-verification is a skill published in the GitHub repository OutlineDriven/odin-claude-plugin (35 stars, last pushed yesterday), licensed Apache-2.0. It adds 36 tokens to every session and 934 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 Code Security Testing claude-code-plugin claude-code-plugins claude-marketplace claude-plugins outline-driven-development

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