Getting it into your agent
One page per mod, every tool's command on it. A separate URL per tool would split the same page into five that compete with each other.
npx skills add dslsdzc/rev-skills --skill re-z3git clone --depth 1 https://github.com/dslsdzc/rev-skillsWrote this? Show the measurements
A badge with what this costs and how it scanned, read live from this page, so it follows the numbers instead of freezing them. Markdown for a README, HTML for a documentation site or a project page.
[](https://agentmods.dev/skills/dslsdzc/rev-skills/re-z3)<a href="https://agentmods.dev/skills/dslsdzc/rev-skills/re-z3"><img src="https://agentmods.dev/badge/skills/dslsdzc/rev-skills/re-z3/github.svg" alt="Measured on agentmods" height="20"></a>Or the 80×15 button, for a site that already has a row of RSS and ATOM ones. Only the verdict fits; the numbers stay here.
<a href="https://agentmods.dev/skills/dslsdzc/rev-skills/re-z3"><img src="https://agentmods.dev/badge/skills/dslsdzc/rev-skills/re-z3.svg" alt="Reviewed on agentmods" width="80" height="20"></a>- NVIDIA SkillSpector pass
What it costs to keep this loaded
Counted locally with the o200k_base tokenizer, which is exact for GPT models; Claude uses its own tokenizer and its counts differ. Treat this as one consistent yardstick across the catalogue rather than a bill. Prices are per million input tokens.
| Model | Per session | Once invoked |
|---|---|---|
| Fable 5.1 | $0.00038 | $0.03446 |
| Opus 5 | $0.00019 | $0.01723 |
| Sonnet 5 | $0.00008 | $0.00689 |
| Haiku 4.5 | $0.00004 | $0.00345 |
Grade A, and why
re-z3 scanned grade A with 0 findings against 26 rules in 11 categories — prompt injection, anti-refusal, data exfiltration, privilege escalation, supply chain, agent snooping, system-prompt leakage, SSRF and excessive agency — measured 9d ago.
A static scan of the body, not an audit. Every finding is printed with the line that produced it so you can judge whether it matters here. A mod is markdown that instructs an agent; that is exactly why what it instructs is worth reading.
Nothing flagged
None of the 26 patterns this scan looks for appear in this file: no shell pipes, no recursive deletes, no credential paths, no hidden text, no instruction-override or anti-refusal phrasing, no agent-config snooping. That is not a guarantee, it is the absence of the things that are checkable.
How it starts
The opening of the file, as written. The whole thing — 103 lines — stays where its author put it; the contents beside it link to each section on GitHub.
Z3 约束求解（建模 / 密钥与 flag 推导）
何时使用 / 何时不用
- 用：从反编译还原出一组"合法输入必须满足"的比较链 / 数学等式（如序列号 = f(用户名)、flag 逐字节满足某关系），直接逆推繁琐时交给求解器
- 用：CTF 逆向题 / 加密题的密钥 / flag 推导（校验逻辑是纯确定性计算，无系统调用依赖）
- 用：已有人工展开的循环体（逐位 XOR / 移位 / 加减）约束，想验证约束集是否完备（见坑 4）
- 不用：输入在长循环里逐字节校验、循环未展开——先 [[re-angr]] 符号执行或先人工展开（本技能要求约束先还原成表达式，见坑 2）
- 不用：约束含哈希 / 非对称验签等不可逆运算——Z3 对 SHA / RSA 验签无能为力（见坑 3）
- 不用：需要整条路径条件而非约束集合——[[re-angr]] 更合适
- 注意：建模必须逐行对照反编译伪代码（[[re-ghidra]] / [[re-ida]] / [[re-radare2]] 产物）；求解出的结果跑原程序验证（沙箱，[[platform-tips]] 最高原则）
工具准备
参考 [[platform-tips]] 最高原则——求解本身不执行目标，但用求解结果运行目标验证时默认沙箱。
z3-solver（pip 安装）
pip install z3-solver（Linux / macOS / Windows 均提供预编译 wheel；纯 Python 绑定 + 原生库，安装简单）- 若与系统包管理器混装冲突（系统 z3 版本旧）：先
pip install --upgrade z3-solver，或独立 venv 内安装 - 验证:
python3 -c "import z3; print(z3.get_version_string())" - 无网络环境：离线 wheel（
pip download z3-solver后拷入）或系统包apt install z3（注意系统 z3 的 python 绑定与 pip 版 API 差异，推荐 pip 版）
python3
- Linux:
apt install python3（多数自带）；macOS:brew install python；Windows: 官方安装包 /choco install python - 验证:
python3 --version
反编译产物（约束还原的原料）
- [[re-ghidra]] / [[re-ida]] / [[re-radare2]] 对校验函数的反编译伪代码——比较链、每次算术 / XOR / 查表变换、最终比对方式（strcmp / 校验位 / 逐位比较）；导出函数级伪代码，作为逐行建模的对照（见坑 4）
- 验证: 伪代码能完整覆盖"合法输入必须满足"的每一条约束
操作步骤
按顺序执行，每步记录结果（约束清单 / 建模脚本 / 求解输出 / 验证结果，证据路径见 [[re-triage]]）。
-
从反编译还原约束（比较链 / 数学关系）：
- 列出"合法输入必须满足"的每条约束：输入来源（用户输入 / 文件名 / 密文）、每次变换（算术 / XOR / 移位 / 查表）、最终比对方式（
if (a == b)/ 校验位相等 / 逐字节 strcmp） - 逐条转成数学表达式，写成清单（伪代码行 → 约束式，一一对应，见坑 4）：
if (x * 3 + 5 != 0x100) fail→x*3 + 5 == 0x100- 循环已展开：
for (i=0;i<8;i++) out[i]=in[i]^key[i]; if(strcmp(out, s)) fail→ 8 条in[i]^key[i] == s[i]
- 不要跳过任何一行——跳过的行就是漏掉的约束（见坑 4）；遇到不可逆段（哈希）先标记，见坑 3
- 列出"合法输入必须满足"的每条约束：输入来源（用户输入 / 文件名 / 密文）、每次变换（算术 / XOR / 移位 / 查表）、最终比对方式（
-
BitVec / Int 建模：
- 位运算为主（XOR / 移位 / 按位与）→ 用 BitVec，位宽对齐反编译语义（32 位运算用
BitVec('x', 32)，逐字节用 8 位） - 纯数学关系（加减乘、比较大小、无位运算）→ 用 Int 更快（但溢出语义与 C 不同，见坑 5）
- 按输入结构建模：字符逐位处理 → 一个 8 位 BitVec 数组或用大 BitVec 切片：
from z3 import * s = Solver() inp = [BitVec(f'inp_{i}', 8) for i in range(8)] # 8 字节输入 - 位宽不匹配立即出问题：
BitVec(..., 8)与BitVec(..., 32)直接相加会报 TypeError / 无解——宽度统一，见坑 5
- 位运算为主（XOR / 移位 / 按位与）→ 用 BitVec，位宽对齐反编译语义（32 位运算用
What this file has done since we first saw it
Hashed on every crawl. A supply-chain change to an agent config is a question of when, not whether, so the history is kept rather than the latest state alone.
- 9d ago First seen · 103 lines · 38 tokens per session scan A 2b8161dd6dc1
re-z3 is a skill published in the GitHub repository dslsdzc/rev-skills (54 stars, last pushed 14d ago), licensed Apache-2.0. It adds 38 tokens to every session and 3,446 once invoked, about $0.0002 per session on Opus 5. A static security scan graded it A with 0 findings. No closer match exists in the catalogue, so it is treated as the original; first seen 2026-09-03.
Other skills, from other repositories
Reverse Engineering & Binary Analysis
Binary analysis, assembly interpretation, disassembly, decompilation, firmware RE, and protocol reverse engineering.
deobfuscating-powershell-obfuscated-malware
Systematically deobfuscates multi-layer PowerShell malware using AST analysis, dynamic tracing, and tools like PSDecode and PowerDecode to reveal hidden payloads and C2 infrastructure. Use during incident response or malware analysis when a PowerShell script is obfuscated with encoding, string manipulation, or…
conducting-malware-incident-response
Respond to malware infections across enterprise endpoints by identifying the malware family, determining infection vectors, assessing spread, and executing containment, analysis, eradication, and recovery procedures aligned to MITRE ATT&CK. Use when responding to a confirmed or suspected malware infection, including…
analyzing-golang-malware-with-ghidra
Reverse engineer Go-compiled malware in Ghidra by parsing Go buildinfo and pclntab structures, recovering stripped/obfuscated function names (e.g. via GoResolver), and extracting embedded module/dependency strings and types from Go binaries. Use when analyzing a Go-language malware sample, deobfuscating a…
analyzing-network-covert-channels-in-malware
Detect and analyze covert communication channels used by malware, including DNS tunneling, ICMP exfiltration, steganographic HTTP, and other protocol abuse used for C2 and data exfiltration. Use when investigating suspicious DNS/ICMP/HTTP traffic patterns, hunting for hidden C2 channels in network captures, or…
analyzing-golang-malware-with-ghidra
Reverse engineer Go-compiled malware using Ghidra with specialized scripts for function recovery, string extraction, and type reconstruction in stripped Go binaries.