ctac ✈️

Python library and CLI for Certora TAC program dumps (.tac and .sbf.json). SeaTac vibes: taxiway maps for TAC CFGs. 🛫🛬

A quick map of what ctac gives you beyond grep:

Purpose	Commands
Inspect a TAC file	stats, parse, pp, cfg, search (alias: grep), slice
Compare two builds	op-diff, cfg-match, bb-diff, sbf-tac
Analyze data-flow	df, types, absint
Transform TAC	rw (rewrites + DCE), ua (uniquify asserts), strip (remove client metadata), pin (specialize), cfg-simplify
Verify	run (concrete interpreter), smt (SMT-LIB VC + z3), verify-cover
Validate the rewriter	rw-valid

Every command has its own --help (full flags + examples in the epilog) and --agent (terse agent-oriented guidance with "why beat manual" framing). The rest of this README is a map, not a manual — drill into --help for flag-level detail.

Environment 🧳

Python 3.11+ (3.14 is fine). From the repo root:

With uv:

uv sync
uv run ctac --help
uv run pytest

uv sync installs the project and its development dependencies into .venv; use uv run to run commands in that environment.

With pip:

python3.14 -m venv .venv
.venv/bin/pip install -U pip
.venv/bin/pip install -e ".[dev]"

Run tools with .venv/bin/ctac or source .venv/bin/activate.

Shell completion (one-time setup; tab-completes commands, subcommands, flag values — and ctac search's pattern against the TAC operator name set):

ctac --install-completion       # auto-detects zsh / bash / fish / powershell
# restart shell

Typical pipelines 🛫

Solve an assertion end-to-end:

ctac stats f.tac --plain  # first look: memory capability + block/cmd counts
ctac rw f.tac -o opt.tac --plain  # simplify (div/bitfield/Ite + DCE)
ctac ua opt.tac -o sa.tac --plain  # fold asserts into one __UA_ERROR block
ctac smt sa.tac --plain --run --model m.txt  # VC + z3, write SAT model
ctac run sa.tac --plain --model m.txt --trace  # replay concretely

Compare two builds (did the encoder drift?):

ctac op-diff a.tac b.tac --plain  # per-stat frequency delta, by section
ctac cfg-match a.tac b.tac --plain  # block correspondence (for bb-diff)
ctac bb-diff a.tac b.tac --plain --drop-empty  # per-block semantic delta

Validate the rewriter itself:

ctac rw-valid -o /tmp/rwv --plain  # emit per-rule SMT soundness scripts
for f in /tmp/rwv/*.smt2; do echo -n "$(basename $f): "; z3 "$f" -T:5; done
# expected `unsat` on every script

Commands 🗺️

Inspect

ctac stats f.tac --plain  # blocks/cmds/metas/ops + memory capability
ctac stats path/to/output-dir --plain  # auto-resolves outputs/*.tac

ctac pp f.tac --plain  # humanized TAC (slices, ceil-div, etc.)
ctac pp f.tac --plain --from A --to B  # slice on a CFG path
ctac pp f.tac -o out.htac  # write pretty-printed text

ctac cfg f.tac --plain  # goto-style CFG text (default)
ctac cfg f.tac --plain --style edges  # `src -> dst` per line, grep-friendly
ctac cfg f.tac --plain --style dot | dot -Tsvg -o cfg.svg
ctac cfg f.tac --plain --style blocks  # one block id per line, shell loops

ctac search f.tac 'BWAnd' --plain --count  # count op usage (tab-completes)
ctac search f.tac 'BWAnd' --plain -C 2  # grep-style context (-B / -A / -C)
ctac search f.tac '0x[0-9a-f]+' --plain --count-by-match  # frequency table
ctac search f.tac 'BWAnd' --plain -q --count  # pipeable; awk on `matches:`

ctac slice f.tac -c B1054 --plain  # backward static slice from a symbol/block

ctac smtlib stats f.smt2 --plain  # for .smt2 inputs: kinds, sorts,
                                  # bytemap chain depth, UF-arg vars
ctac smtlib pp f.smt2 --width 100  # pretty-print via Doc algebra
ctac smtlib slice f.smt2 --kinds Assert --range 0-200  # filter view
ctac smtlib roundtrip f.smt2  # parse + emit; check byte-identical

cfg, pp, search, and df all share the same filter grammar — --from, --to, --only, --id-contains, --id-regex, --cmd-contains, --exclude — combining with AND.

ctac smtlib operates on SMT-LIB v2 files (the output of ctac smt or any external .smt2). It's distinct from ctac smt, which is the TAC→SMT encoder.

Compare two builds

ctac op-diff a.tac b.tac --plain  # per-stat delta, headline in one shot
ctac op-diff a.tac b.tac --plain --show expression_ops
ctac op-diff a.tac b.tac --json  # machine-readable

ctac cfg-match a.tac b.tac --plain --const-weight 0.2
ctac bb-diff  a.tac b.tac --plain --drop-empty --max-diff-lines 120

ctac sbf-tac f.sbf.json f.tac --plain  # join SBF instrs with same-address TAC

op-diff is the fastest way to spot encoder-level drift between two Prover versions (it's built on top of ctac stats). Reach for cfg-match + bb-diff for block-level structural / semantic diffs.

Analyze data-flow

ctac df f.tac --plain  # all analyses, summary
ctac df f.tac --plain --show dsa  # validate DSA (rejecter for sea_vc)
ctac df f.tac --plain --show dce --details  # per-item dead-code listing
ctac df f.tac --plain --json  # machine-readable

ctac types f.tac --plain --show ptr  # kind inference: provable pointers
ctac absint f.tac --plain  # abstract-interpreter analyses (polynomial degree, ...)

Available analyses: def-use, liveness, dce, use-before-def, dsa, control-dependence, uce (useless-assume elimination).

Transform TAC

ctac rw f.tac --plain --report  # simplify + print per-rule hit counts
ctac rw f.tac -o small.tac --plain  # write a round-trippable .tac
ctac rw f.tac -o small.htac --plain  # write pretty-printed .htac
ctac rw f.tac --purify-div --plain  # enable R4a div purification (off by default)

ctac ua f.tac -o f_ua.tac --plain  # fold asserts into one __UA_ERROR block
ctac ua f.tac -o f_ua.tac --plain --report  # + counts

ctac strip f.tac -o f_open.tac --plain --report  # remove client metadata

ctac pin f.tac --drop B7 --bind R3=0 -o sp.tac --plain  # specialize the CFG
ctac cfg-simplify f.tac -o out.tac --plain  # drop annotation-only fall-through blocks

rw runs the iterated simplification pipeline (N1–N4 bit-op canonicalization, R1–R4 div rules, R6 ceil-div collapse, boolean/Ite cleanup, CSE, copy-prop). --purify-div (off by default) adds R4a div purification; --purify-ite / --purify-assert / --purify-assume control post-DCE naming phases. Soundness of every rule is documented by ctac rw-valid.

ua is the prerequisite for ctac smt on multi-assert TAC: it emits if (P) goto GOOD else goto __UA_ERROR for each assert, with assume P opening the GOOD continuation — Floyd-Hoare style, no inversion.

strip removes client-identifying metadata (spec paths, embedded source, function names, call-trace snippets) so a dump can be shared as an open benchmark, keeping the generic structural metadata solvers care about. Unknown keys are dropped by default and flagged in --report.

Verify

ctac run f.tac --plain  # concrete interpreter, zero-havoc
ctac run f.tac --plain --model m.txt --trace  # replay z3 model (TAC or SMT)
ctac run f.tac --plain --model m.txt --validate  # compare computed vs model

ctac smt f.tac --plain  # emit SMT-LIB VC to stdout
ctac smt f.tac --plain -o out.smt2  # write .smt2
ctac smt f.tac --plain --run  # invoke z3
ctac smt f.tac --plain --run --model out.model.txt  # TAC-format SAT model
ctac smt f.tac --plain --run --unsat-core  # name asserts, print core on unsat

ctac z3 f.smt2  # single-run live progress + bottleneck signature
ctac z3 f.smt2 --seeds 0-7 -j 4  # seed sweep race; first verdict wins
ctac z3 f.smt2 --configs default,alt-then,bp-off --seeds 0-3 -j auto
ctac z3 f.smt2 --show-output --save-rerun winner.sh  # capture winner artifacts
ctac z3 --list-configs  # see available configs (defaults + discovered file)

ctac verify-cover cover.json --plain  # re-verify a cover certificate via z3

ctac z3 runs z3 on an existing .smt2 with classification + parallel orchestration. It spawns z3 with -v:2 -st, parses stderr into a progress timeline, and infers a bottleneck signature (fast-close / lp-bp-blowup / nlsat-stuck / nlsat-dominant / etc.). Configs come from a default set (default, alt-then, qfnra-nlsat, bp-off, no-propagate-eqs, legacy-arith); drop a .ctac-z3-configs.json next to the input to add custom named configs. Binary resolution: --z3 PATH / CTAC_Z3 env / $PATH.

ctac smt requires loop-free, single-assert TAC (run ua first); any bytemap capability is supported (bytemap-rw is encoded via Store/Select). The default encoder is sea_vc — QF_UFNIA, DSA + block-reachability, sound bv256 domain constraints, bytemap-as-UF with a per-application range axiom.

ctac run interprets the program concretely — assume failures stop the run silently (infeasible path), assert failures continue and count toward assert_fail. Bytemap symbols load from model entries (both TAC and raw z3 formats) and feed Select lookups.

Validate the rewriter

ctac rw-valid -o /tmp/rwv --plain  # emit all per-rule SMT specs
ctac rw-valid -o /tmp/rwv --plain --rule R4a  # one rule only

Emits a self-contained .smt2 per rule (plus manifest.json) whose expected outcome is unsat. Currently covers R4 (5 operator variants), R4a (base + signed), R6 (base + signed). Other rules are listed in manifest.json:missing.

Manage a project

ctac prj init f.tac -o mytac --plain          # create a project, HEAD = base
ctac prj list mytac --plain                   # show all objects + labels
ctac prj info mytac base --recursive --plain  # walk parents back to base
ctac prj label mytac <sha> tip --plain        # name an object
ctac prj rewind mytac --plain                 # HEAD back to base; keep artifacts
ctac prj reset mytac --plain                  # back to init state; delete derived
ctac prj export-path mytac                    # abs path to HEAD (shell-pipe)
ctac prj archive mytac -o snap.tar.gz --plain # pack .ctac/ for sharing
ctac prj clone snap.tar.gz -o restored        # extract + rebuild symlinks

A project is a working directory with a .ctac/ sidecar that pins HEAD ("the current TAC"), records every produced artifact's provenance, and exposes friendly-name symlinks (base.tac, base.rw.tac, ...) on top of the content-addressed .ctac/objects/ store. Link names derive from the project label (default base, or --label NAME), not the original long filename — that path is kept as source provenance, shown by prj list / prj info. Pass the project directory to rw, ua, pp, smt, or pin in place of a .tac path — HEAD is read for input, and outputs are ingested into the project automatically when -o is omitted:

ctac rw mytac --plain    # HEAD: base.tac -> base.rw.tac
ctac ua mytac --plain    # HEAD: base.rw.tac -> base.rw.ua.tac
ctac smt mytac --plain   # writes base.rw.ua.smt2 as a HEAD sibling

Filesets (directories of TAC files) are first-class. pin --split and ua --strategy split produce a tac-set object; HEAD advances to the fileset (e.g. base.ua.split/). Pick a member with prj set-head to continue:

ctac ua mytac --strategy split --plain          # HEAD -> base.ua.split/
ctac prj list mytac base.ua.split --plain       # show members + hint
ctac prj set-head mytac base.ua.split:assert_01.tac --plain
ctac smt mytac --plain                          # solve the focused case

The library surface (ctac.project.Project) is what the REPL and other tooling should use; the CLI is a thin façade.

Directory input conventions

• TAC inputs: a directory argument is scanned as <dir>/outputs/*.tac, ignoring -rule_not_vacuous files. If multiple candidates remain, ctac warns and picks deterministically.
• Model inputs (run --model <dir>, --fallback <dir>): resolved from <dir>/Reports/ctpp_<rule>-Assertions.txt for the selected TAC's rule. Non-Assertions suffixes emit a warning and are skipped.
• Text commands (parse, stats, search, cfg, pp, cfg-match, bb-diff) accept either .tac or .sbf.json directly.

Library 🏗️

The Python API mirrors the CLI surface. Major modules:

from ctac.parse     import parse_path          # .tac / .sbf.json -> TacFile
from ctac.graph     import Cfg, CfgFilter      # CFG with filtering + rendering
from ctac.analysis  import (                   # data-flow passes + classifiers
    analyze_dsa, analyze_liveness, eliminate_dead_assignments,
    classify_bytemap_usage, BytemapCapability,
)
from ctac.rewrite   import rewrite_program     # rewrite driver
from ctac.rewrite.rules import simplify_pipeline, purify_pipeline
from ctac.ua        import uniquify_asserts, merge_asserts
from ctac.eval      import RunConfig, run_program, parse_model_path, MemoryModel
from ctac.smt       import build_vc, render_smt_script

One worked example — slice a CFG between two blocks:

from ctac.parse import parse_path
from ctac.graph import Cfg, CfgFilter

tac = parse_path("f.tac")
cfg = Cfg(tac.program)
sliced, warnings = cfg.filtered(CfgFilter(from_id="entry", to_id="exit"))
print(f"{len(sliced.blocks)} blocks on some path from entry to exit")

End-to-end — rewrite, uniquify, build VC:

import dataclasses
from ctac.parse import parse_path
from ctac.rewrite import rewrite_program
from ctac.rewrite.rules import default_pipeline
from ctac.ua import uniquify_asserts
from ctac.smt import build_vc, render_smt_script

tac = parse_path("f.tac")
rw  = rewrite_program(tac.program, default_pipeline)
ua  = uniquify_asserts(rw.program)
vc  = build_vc(dataclasses.replace(tac, program=ua.program))
print(render_smt_script(vc))

Editor integration

A VSCode extension for the humanized TAC output of ctac pp (.htac) and rendered SBF files (.sbf) lives in tools/vscode-tac/ — syntax highlighting, go-to-definition for block targets and variables, and find-references for variables. It is not published to the marketplace yet; build and install locally:

cd tools/vscode-tac
just package-install  # package the .vsix and install into `code`

Without just:

cd tools/vscode-tac
npx @vscode/vsce package
code --install-extension ctac-vscode-*.vsix

See tools/vscode-tac/README.md for file-association tips (e.g. treating tac1.txt / tac2.txt as htac without renaming).

Claude Code integration 🤖

ctac-fly is a Claude Code skill that recognizes TAC-investigation intent in a Claude session and routes to the right ctac command — instead of letting the agent fall back to ad-hoc grep on raw .tac files. It ships as a marketplace-of-one; install inside any Claude Code session:

/plugin marketplace add https://github.com/1arie1/ctac-fly.git
/plugin install ctac-fly@ctac-fly

The skill assumes ctac is already on PATH (set up per Environment). When a command needs z3, the skill instructs the agent to use ctac smt --run --z3-path <path> rather than mutating the user's PATH.

Authors

• Arie Gurfinkel arie@certora.com

AI collaborators

Generative-AI coding tools contributed implementation, tests, and documentation under direction. Design decisions, scope control, and final review rest with the human authors above; all AI contributions were reviewed and committed by a human.

• Cursor (OpenAI-backed models, e.g. Codex) — Made-with: Cursor commit trailers.
• Claude Code (Anthropic Claude Opus 4.x) — Co-Authored-By: Claude ... commit trailers.
• Occasional use of editor-integrated assistants that do not emit trailers.

Per-change attribution is in git history (git log --grep='Made-with', git log --grep='Co-Authored-By: Claude').

License

MIT. See LICENSE.