solve

Check satisfiability of SMT-LIB2 formulas using Z3. Returns sat/unsat with models or unsat cores. Logs every invocation to z3agent.db for auditability.

Quality

81%

Does it follow best practices?

Run evals on this skill

Adds up to 20 points to the overall score

View guide

Securityby

Passed

No findings from the security scan

Quality

Content

93%Weight 40%Scale 1-5

Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.

A tight, highly actionable skill body: executable commands, an accurate parameter table, and a clear three-step workflow with outcome-based interpretation. The only notable gap is that the timeout/unknown recovery path in Step 3 doesn't explicitly close the loop back to re-running the solver.

Dimension	Reasoning	Score
Conciseness	The body is lean and assumes Claude's competence: it never explains what Z3, SMT-LIB2, or satisfiability are, and the Action/Expectation/Result blocks each carry distinct information (input contract, output contract, branching) rather than padding. Nothing to trim.	5 / 5
Actionability	Fully executable, copy-paste-ready commands covering the common cases (formula string, file input, debug tracing), plus a complete parameter table with types, defaults, and the 'Either formula or file must be provided' constraint. All flags match the actual scripts/solve.py implementation.	5 / 5
Workflow Clarity	A clear three-step sequence with an input validation checkpoint in Step 1 and per-outcome handling in Step 3, including a recovery path ('On unknown/timeout: try simplify or increase the timeout'). Not a 5 because the feedback loop is weakly specified: it never explicitly returns to Step 2 to re-run after a timeout, and there is no check that the z3 binary is available.	4 / 5
Progressive Disclosure	Well-organized sections with the single bundle file (scripts/solve.py) referenced exactly where used, real on disk, and one level deep; the parameter table is correctly kept inline rather than split out. No organization gaps.	5 / 5
	Total	19 / 20 Passed

Description

70%Weight 40%Scale 1-5

Based on the skill's description, can an agent find and select it at the right time? Clear, specific descriptions lead to better discovery.

A concise, concrete, third-person description that clearly states what the skill does and sits in a well-distincted niche. Its main weakness is the complete absence of any 'Use when...' trigger guidance, which both caps completeness and leaves activation to inference.

Suggestions

Append an explicit trigger clause, e.g. 'Use when the user asks whether a formula or constraint set is satisfiable, mentions SMT, Z3, or .smt2 files, or wants a model or unsat core.'

Mention natural-language constraint input as a supported input mode, since the body routes such inputs through the encode skill — currently the description only advertises SMT-LIB2 formulas.

Add common synonyms/extensions (.smt2, 'solver', 'constraints') to improve trigger term coverage toward the comprehensive level.

Dimension	Reasoning	Score
Specificity	Lists several concrete actions ('Check satisfiability of SMT-LIB2 formulas', 'Returns sat/unsat with models or unsat cores', 'Logs every invocation') but omits capabilities the skill actually has, such as natural-language constraint input and the encode-skill integration. It exceeds the 1-2 actions of anchor 3 but has the minor coverage gaps of anchor 4.	4 / 5
Completeness	The 'what' is clearly and concretely stated, but there is no 'Use when...' clause or any equivalent explicit trigger guidance, which caps completeness at 3 per the judging guidelines.	3 / 5
Trigger Term Quality	Good natural keyword coverage a user would actually say ('satisfiability', 'SMT-LIB2', 'Z3', 'sat/unsat', 'unsat core'), but no synonyms or file extensions like '.smt2' or 'solver', which anchor 5 requires.	4 / 5
Distinctiveness Conflict Risk	Occupies a clear niche (SMT satisfiability checking via Z3) with highly distinct trigger terms ('SMT-LIB2', 'Z3', 'unsat core'); minimal conflict risk with other skills.	5 / 5
	Total	16 / 20 Passed

Validation

100%

Warnings & errors only

Checks the skill against the spec for correct structure and formatting. All validation checks must pass before discovery and implementation can be scored.

Validation — 16 / 16 Passed

Validation for skill structure

No warnings or errors.

Repository: Z3Prover/z3
Path: .github/skills/solve/SKILL.md
Commit: dabaa0b

Reviewed: 7 days ago

Table of Contents

Discovery Implementation Validation

Is this your skill?

If you maintain this skill, you can claim it as your own. Once claimed, you can manage eval scenarios, bundle related skills, attach documentation or rules, and ensure cross-agent compatibility.