simplify

Reduce formula complexity using Z3 tactic chains. Supports configurable tactic pipelines for boolean, arithmetic, and bitvector simplification.

Quality

83%

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

100%

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

The body is lean, actionable, and well-structured with executable examples, a clear sequenced workflow, and a feedback loop. It appropriately offloads detail to a real referenced script without nested or dangling references.

Dimension	Reasoning	Score
Conciseness	Lean and efficient with no over-explanation of concepts Claude already knows; the Action/Expectation/Result structure, tactic table, and parameter table each earn their tokens without padding.	3 / 3
Actionability	Provides fully executable bash invocations referencing the real scripts/simplify.py, a concrete tactic table, and a complete parameter table with defaults — copy-paste ready.	3 / 3
Workflow Clarity	Clear three-step sequence (choose tactics → run → interpret) with an explicit feedback loop ('If unchanged, try a different tactic chain') for error recovery.	3 / 3
Progressive Disclosure	Well-organized sections with a single one-level-deep, real script reference (verified scripts/simplify.py exists); appropriately structured for a compact single-purpose skill.	3 / 3
	Total	12 / 12 Passed

Description

67%

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

The description is specific and well-scoped to Z3 formula simplification with concrete actions and clear distinctiveness. Its main weakness is the absence of an explicit 'Use when…' trigger clause and incomplete coverage of common Z3/SMT user terminology.

Suggestions

Add an explicit 'Use when…' clause, e.g. 'Use when simplifying or reducing SMT-LIB2 formulas, debugging Z3 tactic selection, or preprocessing formulas before solving or proving.'

Include natural user trigger terms such as 'SMT', '.smt2', 'SMT-LIB2', 'prove', and 'solve' alongside the existing Z3/tactic vocabulary.

Dimension	Reasoning	Score
Specificity	Lists multiple concrete actions — 'Reduce formula complexity using Z3 tactic chains' and 'configurable tactic pipelines for boolean, arithmetic, and bitvector simplification' — covering specific operations and theories rather than vague language.	3 / 3
Completeness	Clearly answers 'what' the skill does but lacks any 'Use when…' trigger clause or equivalent explicit 'when' guidance, which caps completeness at 2 per the rubric guidelines.	2 / 3
Trigger Term Quality	Includes relevant natural terms ('formula', 'Z3', 'tactic', 'simplification', 'bitvector') but omits common Z3-user phrasings like 'SMT', '.smt2', 'prove', or 'solve' that users would naturally say.	2 / 3
Distinctiveness Conflict Risk	Targets a clear niche — Z3 tactic-based formula simplification — with distinct terminology, making it unlikely to trigger for unrelated skills.	3 / 3
	Total	10 / 12 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/simplify/SKILL.md
Commit: 1c89937

Reviewed: 3 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.