How do I install the Formalize skill?

Run npx skillmds@latest add ddaanet/formalize in your terminal (requires Node.js), paste this page's agent-chat prompt into Claude, Cursor, or any MCP-connected agent, or download the SKILL.md file and copy it into your agent's skills directory.

Is Formalize safe to use?

This skill has not completed SkillMD's automated safety review yet. Capability flags: docs only. SkillMD never runs a skill's scripts for you; review the SKILL.md before installing.

Which AI agents work with Formalize?

This skill is tagged as working with Claude Code, Claude.ai, OpenAI Codex. SKILL.md is an open format, so most agents that read a skills directory can load it too.

Is Formalize free to use?

Yes. Installing skills from SkillMD is free, and the skill stays under its author's original license.

Who published Formalize?

ddaanet (@ddaanet) published this skill. Their other Agent Skills are listed on their SkillMD profile.

Formalize by ddaanet — Agent Skill

Name: Formalize
Rating: 4.2 (5 reviews)
Author: ddaanet

Formalize

Verify a Python function against its intended behavior by writing an icontract contract and checking it with `edify check` (CrossHair), repairing in a loop. Triggers on "formalize", "verify this function", "add a contract and check it", or after writing a function whose correctness matters. The in-context agent holds intent and asks the user when behavior is ambiguous; CrossHair owns the deduction.

ddaanet Updated Sep 10, 2026

File contents

Formalize and Check a Function

Drive a propose-contract -> check -> repair loop around one Python function. The verifier (edify check, backed by CrossHair) owns deduction. You own intent: what the function should guarantee. Verification proves code meets a contract; it does NOT prove the contract is the right one. That judgment is yours, and when intent is genuinely ambiguous you ASK rather than guess.

Procedure

Establish intent. Derive what the target function should guarantee from the conversation and the surrounding code. If the intended behavior is genuinely ambiguous (edge cases, error handling, empty inputs), use AskUserQuestion — do not invent a specification.
Write the contract. Add icontract decorators to the function: @require(lambda <args>: <precondition>) and @ensure(lambda <args>, result: <postcondition>). A target needs at least one pre/post-condition or CrossHair will not analyze it.
Check. Run:
```
edify check <file-or-dotted-target> --json
```
The result status is one of verified, refuted, or error.
Interpret — the core judgment:
- verified — no counterexample within CrossHair's search budget. Report and stop. State the honest guarantee level: bounded path-exploration, not a total proof.
- refuted — read the counterexample (falsifying input + location), then decide why it failed:
  - code bug — the implementation is wrong: fix the code.
  - spec bug — the contract was wrong or too strong: fix the contract.
  - intent ambiguity — the counterexample exposes a case the user has not decided (e.g. "what should this do on an empty list?"): STOP and ask. Then loop back to step 3.
- error — surface it. A common cause is a target with no contract (CrossHair analyzed nothing); add a contract. Never report error as success.
Loop with a cap. Do at most a small fixed number of repair iterations (e.g. 5). If you hit the cap, STOP and report the honest state: the last counterexample and what remains unresolved. Never upgrade refuted or an error to "verified".

Disciplines

Ambiguity about intent -> ask, never guess.
Every counterexample gets an explicit code-bug vs spec-bug triage.
No "verified" claim without a verified result from edify check.
A verified result is bounded, not a soundness/termination proof — say so.

Backend

edify check wraps CrossHair (symbolic execution + Z3). It is the deduction oracle; this skill is the intent-holder. See docs/superpowers/specs/2026-06-08-invariant-guided-verify-loop-design.md.

---name: formalizedescription: Verify a Python function against its intended behavior by writing an icontract contract and checking it with `edify check` (CrossHair), repairing in a loop. Triggers on "formalize", "verify this function", "add a contract and check it", or after writing a function whose correctness matters. The in-context agent holds intent and asks the user when behavior is ambiguous; CrossHair owns the deduction.---# Formalize and Check a FunctionDrive a propose-contract -> check -> repair loop around one Python function.The verifier (`edify check`, backed by CrossHair) owns deduction. You own*intent*: what the function should guarantee. Verification proves code meets acontract; it does NOT prove the contract is the right one. That judgment isyours, and when intent is genuinely ambiguous you ASK rather than guess.## Procedure1. **Establish intent.** Derive what the target function should guarantee from the conversation and the surrounding code. If the intended behavior is genuinely ambiguous (edge cases, error handling, empty inputs), use `AskUserQuestion` — do not invent a specification.2. **Write the contract.** Add `icontract` decorators to the function: `@require(lambda <args>: <precondition>)` and `@ensure(lambda <args>, result: <postcondition>)`. A target needs at least one pre/post-condition or CrossHair will not analyze it.3. **Check.** Run: ``` edify check <file-or-dotted-target> --json ``` The result status is one of `verified`, `refuted`, or `error`.4. **Interpret — the core judgment:** - `verified` — no counterexample within CrossHair's search budget. Report and stop. State the honest guarantee level: bounded path-exploration, not a total proof. - `refuted` — read the counterexample (falsifying input + location), then decide *why* it failed: - **code bug** — the implementation is wrong: fix the code. - **spec bug** — the contract was wrong or too strong: fix the contract. - **intent ambiguity** — the counterexample exposes a case the user has not decided (e.g. "what should this do on an empty list?"): STOP and ask. Then loop back to step 3. - `error` — surface it. A common cause is a target with no contract (CrossHair analyzed nothing); add a contract. Never report `error` as success.5. **Loop with a cap.** Do at most a small fixed number of repair iterations (e.g. 5). If you hit the cap, STOP and report the honest state: the last counterexample and what remains unresolved. Never upgrade `refuted` or an error to "verified".## Disciplines- Ambiguity about intent -> ask, never guess.- Every counterexample gets an explicit code-bug vs spec-bug triage.- No "verified" claim without a `verified` result from `edify check`.- A `verified` result is bounded, not a soundness/termination proof — say so.## Backend`edify check` wraps CrossHair (symbolic execution + Z3). It is the deductionoracle; this skill is the intent-holder. See`docs/superpowers/specs/2026-06-08-invariant-guided-verify-loop-design.md`.

Frequently asked questions