Validates logical conjectures by checking the satisfiability of their negation.
Install
mkdir -p .claude/skills/prove-z3prover && curl -L -o skill.zip "https://agentskills.codes/api/skills/download/17804" && unzip -o skill.zip -d .claude/skills/prove-z3prover && rm skill.zipInstalls to .claude/skills/prove-z3prover
Activation
This is the description your AI agent reads to decide when to run this skill — the better it matches your request, the more reliably it fires.
Prove validity of logical statements by negation and satisfiability checking. If the negation is unsatisfiable, the original statement is valid. Otherwise a counterexample is returned.Key capabilities
- →Prepares negated formula for satisfiability checking
- →Invokes prove.py with conjecture and variable declarations
- →Interprets prover output for validity
- →Reports counterexamples for invalid statements
- →Handles unknown or timeout results
- →Logs run entries to z3agent.db
How it works
The skill proves the validity of logical statements by negating the conjecture and checking its satisfiability using a prover.
Inputs & outputs
When to use prove
- →Proving logical implications
- →Finding counterexamples for code logic
- →Validating SMT-LIB2 assertions
About this skill
Given a conjecture (an SMT-LIB2 assertion or a natural language claim), determine whether it holds universally. The method is standard: negate the conjecture and check satisfiability. If the negation is unsatisfiable, the original is valid. If satisfiable, the model is a counterexample.
Step 1: Prepare the negated formula
Action:
Wrap the conjecture in (assert (not ...)) and append
(check-sat)(get-model).
Expectation: A complete SMT-LIB2 formula that negates the original conjecture with all variables declared.
Result: If the negation is well-formed, proceed to Step 2. If the conjecture is natural language, run encode first.
Example: to prove that (> x 3) implies (> x 1):
(declare-const x Int)
(assert (not (=> (> x 3) (> x 1))))
(check-sat)
(get-model)
Step 2: Run the prover
Action: Invoke prove.py with the conjecture and variable declarations.
Expectation:
The script prints valid, invalid (with counterexample), unknown,
or timeout. A run entry is logged to z3agent.db.
Result:
On valid: proceed to explain if the user needs a summary.
On invalid: report the counterexample directly.
On unknown/timeout: try simplify first, or increase the timeout.
python3 scripts/prove.py --conjecture "(=> (> x 3) (> x 1))" --vars "x:Int"
For file input where the file contains the full negated formula:
python3 scripts/prove.py --file negated.smt2
With debug tracing:
python3 scripts/prove.py --conjecture "(=> (> x 3) (> x 1))" --vars "x:Int" --debug
Step 3: Interpret the output
Action: Read the prover output to determine validity of the conjecture.
Expectation:
One of valid, invalid (with counterexample), unknown, or timeout.
Result:
On valid: the conjecture holds universally.
On invalid: the model shows a concrete counterexample.
On unknown/timeout: the conjecture may require auxiliary lemmas or induction.
Parameters
| Parameter | Type | Required | Default | Description |
|---|---|---|---|---|
| conjecture | string | no | the assertion to prove (without negation) | |
| vars | string | no | variable declarations as "name:sort" pairs, comma-separated | |
| file | path | no | .smt2 file with the negated formula | |
| timeout | int | no | 30 | seconds |
| z3 | path | no | auto | path to z3 binary |
| debug | flag | no | off | verbose tracing |
| db | path | no | .z3-agent/z3agent.db | logging database |
Either conjecture (with vars) or file must be provided.
When not to use it
- →When the conjecture is not an SMT-LIB2 assertion or natural language claim
- →When a summary is not needed for valid statements
- →When the user does not want to try simplify or increase timeout for unknown/timeout results
Limitations
- →Requires the conjecture to be well-formed SMT-LIB2 or natural language
- →If the conjecture is natural language, it requires an 'encode' step first
- →May return 'unknown' or 'timeout' for complex conjectures
How it compares
This skill determines universal validity by negating a conjecture and using a satisfiability checker, providing counterexamples for invalid statements, unlike direct logical evaluation.
Compared to similar skills
prove side by side with the closest alternatives in the catalog.
| Skill | Installs | Updated | Safety | Difficulty |
|---|---|---|---|---|
| prove (this skill) | 0 | 4mo | Review | Advanced |
| python-repl | 6 | 4mo | Review | Beginner |
| compare-cpython-versions | 1 | 7mo | Review | Advanced |
| detect-silent-processing-failures | 0 | 4mo | Review | Intermediate |
Try saying
Example prompts that trigger this skill in your AI assistant.
More by Z3Prover
View all by Z3Prover →You might also like
python-repl
gptme
Interactive Python REPL automation with common helpers and best practices
compare-cpython-versions
DataDog
Compare CPython source code between two Python versions to identify changes in headers and structs. Use this when adding support for a new Python version to understand what changed between versions.
detect-silent-processing-failures
atniptw
Use to detect suspicious processor outputs even when no exception is thrown. Keywords: silent failure, metadata validation, glb checks, anomaly detection.
solve
Z3Prover
Check satisfiability of SMT-LIB2 formulas using Z3. Returns sat/unsat with models or unsat cores. Logs every invocation to z3agent.db for auditability.
massgen-log-analyzer
massgen
Run MassGen experiments and analyze logs using automation mode, logfire tracing, and SQL queries. Use this skill for performance analysis, debugging agent behavior, evaluating coordination patterns, and improving the logging structure, or whenever an ANALYSIS_REPORT.md is needed in a log directory.
research
dmitryprg-ai
Analyze data, investigate datasets, debug with data, and explore system behavior. Use when analyzing, running SQL queries, data profiling, investigating patterns, building statistics, exploring CSV/JSON data, or debugging with data evidence.