Z3 Agent

A Copilot agent for the Z3 theorem prover. It wraps 9 skills that cover SMT solving and code quality analysis.

What it does

The agent handles two kinds of requests:

1. SMT solving: formulate constraints, check satisfiability, prove properties, optimize objectives, simplify expressions.
2. Code quality: run sanitizers (ASan, UBSan) and Clang Static Analyzer against the Z3 codebase to catch memory bugs and logic errors.

Prerequisites

You need a built Z3 binary. The scripts look for it in this order:

1. Explicit --z3 path/to/z3
2. build/z3, build/release/z3, build/debug/z3 (relative to repo root)
3. z3 on your PATH

For code quality skills you also need:

• memory-safety: cmake, make, and a compiler with sanitizer support (gcc or clang). The script checks at startup and tells you what is missing.
• static-analysis: scan-build (part of clang-tools). Same early check with install instructions if absent.

Using the agent in Copilot Chat

Mention @z3 and describe what you want in plain language. The agent figures out which skill to use, builds the formula if needed, runs Z3, and gives you the result.

solve: check satisfiability

@z3 is (x > 0 and y > 0 and x + y < 5) satisfiable over the integers?

Expected response: sat with a model like x = 1, y = 1.

@z3 can x + y = 10 and x - y = 4 both hold at the same time?

Expected response: sat with x = 7, y = 3.

@z3 is there an integer x where x > 0, x < 0?

Expected response: unsat (no such integer exists).

prove: check if something is always true

@z3 prove that x * x >= 0 for all integers x

Expected response: valid (the negation is unsatisfiable, so the property holds).

@z3 is it true that (a + b)^2 >= 0 for all real a and b?

Expected response: valid.

@z3 prove that if x > y and y > z then x > z, for integers

Expected response: valid (transitivity of >).

optimize: find the best value

@z3 maximize 3x + 2y where x >= 1, y >= 1, and x + y <= 20

Expected response: sat with x = 19, y = 1 (objective = 59).

@z3 minimize x + y where x >= 5, y >= 3, and x + y >= 10

Expected response: sat with x = 5, y = 5 or similar (objective = 10).

simplify: reduce an expression

@z3 simplify x + 0 + 1*x

Expected response: 2*x.

@z3 simplify (a and true) or (a and false)

Expected response: a.

encode: translate a problem to SMT-LIB2

@z3 encode this as SMT-LIB2: find integers x and y where x + y = 10 and x > y

Expected response: the SMT-LIB2 formula:

(declare-const x Int)
(declare-const y Int)
(assert (= (+ x y) 10))
(assert (> x y))
(check-sat)
(get-model)

explain: interpret Z3 output

@z3 what does this Z3 output mean?
sat
(
  (define-fun x () Int 7)
  (define-fun y () Int 3)
)

Expected response: a readable summary like "satisfying assignment: x = 7, y = 3".

@z3 Z3 returned unknown, what does that mean?

Expected response: an explanation of common causes (timeout, incomplete theory, quantifiers).

benchmark: measure performance

@z3 how fast can Z3 solve (x > 0 and y > 0 and x + y < 100)? run it 5 times

Expected response: timing stats like min/median/max in milliseconds and the result.

memory-safety: find memory bugs in Z3

@z3 run AddressSanitizer on the Z3 test suite

Expected response: builds Z3 with ASan, runs the tests, reports any findings with category, file, and line number. If clean, reports no findings.

@z3 check for undefined behavior in Z3

Expected response: runs UBSan, same format.

@z3 run both sanitizers

Expected response: runs ASan and UBSan, aggregates findings from both.

static-analysis: find bugs without running the code

@z3 run static analysis on the Z3 source

Expected response: runs Clang Static Analyzer, reports findings grouped by category (null dereference, dead store, memory leak, etc.) with file and line.

multi-skill: the agent chains skills when needed

@z3 prove that for all integers, if x^2 is even then x is even

The agent uses encode to formalize and negate the statement, then prove to check it, then explain to present the result.

@z3 full verification pass before the release

The agent runs memory-safety (ASan + UBSan) and static-analysis in parallel, then aggregates and deduplicates findings sorted by severity.

Using the scripts directly

Every skill lives under .github/skills/<name>/scripts/. All scripts accept --debug for full tracing and --db path to specify where the SQLite log goes (defaults to z3agent.db in the current directory).

solve

Check whether a set of constraints has a solution.

python3 .github/skills/solve/scripts/solve.py \
  --z3 build/release/z3 \
  --formula '
(declare-const x Int)
(declare-const y Int)
(assert (> x 0))
(assert (> y 0))
(assert (< (+ x y) 5))
(check-sat)
(get-model)'

Output:

sat
  x = 1
  y = 1

prove

Check whether a property holds for all values. The script negates your conjecture and asks Z3 if the negation is satisfiable. If it is not, the property is valid.

python3 .github/skills/prove/scripts/prove.py \
  --z3 build/release/z3 \
  --conjecture '(>= (* x x) 0)' \
  --vars 'x:Int'

Output:

valid

If Z3 finds a counterexample, it prints invalid followed by the counterexample values.

optimize

Find the best value of an objective subject to constraints.

python3 .github/skills/optimize/scripts/optimize.py \
  --z3 build/release/z3 \
  --formula '
(declare-const x Int)
(declare-const y Int)
(assert (>= x 1))
(assert (>= y 1))
(assert (<= (+ x y) 20))
(maximize (+ (* 3 x) (* 2 y)))
(check-sat)
(get-model)'

Output:

sat
  x = 19
  y = 1

Here Z3 maximizes 3x + 2y under the constraint x + y <= 20, so it pushes x as high as possible (19) and keeps y at its minimum (1), giving 3*19 + 2*1 = 59.

simplify

Reduce expressions using Z3 tactic chains.

python3 .github/skills/simplify/scripts/simplify.py \
  --z3 build/release/z3 \
  --formula '(declare-const x Int)(simplify (+ x 0 (* 1 x)))'

Output:

(* 2 x)
(goals
(goal
  :precision precise :depth 1)
)

Z3 simplified x + 0 + 1*x down to 2*x.

benchmark

Measure solving time over multiple runs.

python3 .github/skills/benchmark/scripts/benchmark.py \
  --z3 build/release/z3 \
  --runs 5 \
  --formula '
(declare-const x Int)
(declare-const y Int)
(assert (> x 0))
(assert (> y 0))
(assert (< (+ x y) 100))
(check-sat)'

Output (times will vary on your machine):

runs: 5
min: 27ms
median: 28ms
max: 30ms
result: sat

explain

Interpret Z3 output in readable form. It reads from stdin:

echo 'sat
(
  (define-fun x () Int
    19)
  (define-fun y () Int
    1)
)' | python3 .github/skills/explain/scripts/explain.py --stdin --type model

Output:

satisfying assignment:
  x = 19
  y = 1

encode

Validate that an SMT-LIB2 file is well-formed by running it through Z3:

python3 .github/skills/encode/scripts/encode.py \
  --z3 build/release/z3 \
  --validate problem.smt2

If the file parses and runs without errors, it prints the formula back. If there are syntax or sort errors, it prints the Z3 error message.

memory-safety

Build Z3 with AddressSanitizer or UndefinedBehaviorSanitizer, run the test suite, and collect any findings.

python3 .github/skills/memory-safety/scripts/memory_safety.py --sanitizer asan
python3 .github/skills/memory-safety/scripts/memory_safety.py --sanitizer ubsan
python3 .github/skills/memory-safety/scripts/memory_safety.py --sanitizer both

Use --skip-build to reuse a previous instrumented build. Use --build-dir path to control where the build goes (defaults to build/sanitizer-asan or build/sanitizer-ubsan under the repo root).

If cmake, make, or a C compiler is not found, the script prints what you need to install and exits.

static-analysis

Run Clang Static Analyzer over the Z3 source tree.

python3 .github/skills/static-analysis/scripts/static_analysis.py \
  --build-dir build/scan

Results go to build/scan/scan-results/ by default. Findings are printed grouped by category with file and line number.

If scan-build is not on your PATH, the script prints install instructions for Ubuntu, macOS, and Fedora.

Debug tracing

Add --debug to any command to see the full trace: run IDs, z3 binary path, the exact command and stdin sent to Z3, stdout/stderr received, timing, and database logging. Example:

python3 .github/skills/solve/scripts/solve.py \
  --z3 build/release/z3 --debug \
  --formula '
(declare-const x Int)
(declare-const y Int)
(assert (> x 0))
(assert (> y 0))
(assert (< (+ x y) 5))
(check-sat)
(get-model)'

[DEBUG] started run 31 (skill=solve, hash=d64beb5a61842362)
[DEBUG] found z3: build/release/z3
[DEBUG] cmd: build/release/z3 -in
[DEBUG] stdin:
(declare-const x Int)
(declare-const y Int)
(assert (> x 0))
(assert (> y 0))
(assert (< (+ x y) 5))
(check-sat)
(get-model)
[DEBUG] exit_code=0 duration=28ms
[DEBUG] stdout:
sat
(
  (define-fun x () Int
    1)
  (define-fun y () Int
    1)
)
[DEBUG] finished run 31: sat (28ms)
sat
  x = 1
  y = 1

Logging

Every run is logged to a SQLite database (z3agent.db by default). You can query it directly:

sqlite3 z3agent.db "SELECT id, skill, status, duration_ms FROM runs ORDER BY id DESC LIMIT 10;"

Use --db /path/to/file.db on any script to put the database somewhere else.

Skill list