KryptosAI/counterflow

# Counterflow [](https://www.npmjs.com/package/@kryptosai/counterflow) [](https://github.com/KryptosAI/counterflow/actions/workflows/ci.yml) [](https://github.com/KryptosAI/counterflow/blob/main/LICENSE) [](https://nodejs.org/) Counterflow 是一个智能合约安全 CLI：提供 AI 翻译、机器证明的形式化验证，专为 Solidity DeFi 合约设计 —— 英文不变量由可信的 Z3/SMT 核心检查，并由符号执行（Halmos, Foundry）和用于不变量测试的 Echidna harness 生成提供支持。包含 5 种模型类型，涵盖 erc20、amm、lending、staking、oracle 和 governance 的 16 个基准测试用例，并重现了 5 个真实的 DeFi 攻击事件（损失超 2.61 亿美元）。 **LLM 绝不决定验证结果。** 一个约 560 行、可供人工审计的 Z3 核心要么为**所有**输入*证明*该不变量，要么生成一个**具体的反例**（攻击轨迹）。 ``` Solidity + English invariants │ ▼ [LLM translate] untrusted — DeepSeek/OpenAI, temperature 0 │ ▼ binding.json human-reviewable artifact (the real spec) │ ▼ [validate] deterministic vocabulary/schema gate (5 models, 27 guards, 43 effects, 33 invariants) │ ▼ [Z3 inductive check] TRUSTED — 5 model types: erc20_pool, amm_pool, lending_pool, staking_pool, cross_contract │ ▼ PROVED | VIOLATED (+ cex) → audit.jsonl (SHA-256 hash-chained) │ ▼ [Halmos bytecode] TRUSTED — EVM symbolic exec (9 scenarios, 3 PASS / 6 FAIL confirming exploits) [Foundry fuzz+symb] fuzz → cex → halmos symbolic proof [Echidna validation] harness generation from binding ``` ## 状态模型 (5 种类型) | 模型 | 词汇表 | 守卫 | 效果 | 不变量 | |---|---|---|---|---| | `erc20_pool` | balances, shares, allowances, totals, ghost sums | 11 | 16 | 10 | | `amm_pool` | reserveX/Y, lpSupply, lpBalances, initialK | 5 | 8 | 5 | | `lending_pool` | collateral, debt, totals, liqThreshold | 3 | 8 | 8 | | `staking_pool` | staked, rewards, totalStaked, rewardPool | 2 | 6 | 5 | | `cross_contract` | cross-in-progress flag, snapshots | 2 | 2 | 1 | | 共享扩展 | oracle (price, twap), governance (timelock) | 4 | 3 | 4 | 所有模型共享重入词汇表（lock/snapshot/external-call）。oracle 和 governance 扩展是可在各模型间使用的共享词汇表。 ## 安装说明 ``` npm install @kryptosai/counterflow # 依赖项：Python 3 + z3-solver (pip install z3-solver) # 可选：halmos (pip install halmos), Foundry (brew install foundry) counterflow doctor # check all deps ``` ## 快速开始 ``` counterflow check examples/TokenPool.binding.json # PROVED counterflow check examples/TokenPoolBuggy.binding.json # VIOLATED + exploit counterflow verify Contract.sol invariants.txt # full AI pipeline (needs API key) counterflow check binding.json # deterministic, no LLM counterflow bytecode HalmosTest # 9 EVM symbolic tests counterflow audit # verify SHA-256 chain ``` ## 基准测试 ``` 16/16 solver cases correct (110-320ms per case): erc20_pool: TokenPool†, SafeVault†, TokenPoolBuggy✗, ApprovalDrain✗, UnbackedMintVault✗, BurnDesyncVault✗ amm_pool: AMMSwap†, AMMPriceManipulation✗ lending: LendingPool†, LendingUnbackedBorrow✗ staking: StakingPool†, StakingInfiniteReward✗ oracle: OracleSafe†, OracleManipulation✗ governance: GovernanceTimelock†, GovernanceNoTimelock✗ 5/5 DeFiHackLabs real exploits reproduced (deterministic, no LLM): FEI Protocol ($80M) reentrancy → reentrancy_safe violated CREAM Finance ($130M) ERC777 reentrancy → nonneg_balance violated PancakeBunny ($45M) flash loan → backing violated OpenLeverage ($230K) access control → backing violated Belt Finance ($6.3M) arithmetic → solvency violated 3/3 ValuePacket contracts PROVED at pool level 22/22 e2e tests pass ``` ## 工作原理 1. 您使用英文或 Solidity 注释编写不变量 2. LLM 翻译合约和不变量 → 结构化绑定 JSON（不可信层） 3. 确定性 Z3 核心证明不变量或生成反例（可信层） 4. 可选的 Halmos 字节码兜底机制弥合规范与实现之间的差距 5. SHA-256 哈希链审计日志记录每次运行 ## Counterflow 与同类工具对比 | | Counterflow | Certora Prover | Kontrol | Halmos | |---|---|---|---|---| | 许可证 | MIT | GPL-3.0 | BSD-3 | AGPL-3.0 | | 输入 | 英文 | CVL spec | Foundry tests | Foundry tests | | 证明层级 | Z3 抽象 | SMT | KEVM 字节码 | 符号执行 | | 多合约 | 是（cross_contract 模型 + Halmos） | 是（场景链接） | 是 | 是 | | 模型类型 | 5（可扩展） | 不限 | 不限 | 不适用 | | 字节码兜底 | Halmos + Foundry | 否 | 原生 | 原生 | | 审计链 | SHA-256 | 云端 | 否 | 否 | | 环境配置 | npm + Python | Java + Gradle | K + Nix | pip | ## 验证结果说明 - **PROVED** — 所建模型的转换对于*所有*可能的输入都保持不变量 - **VIOLATED** — Z3 或 Halmos 找到了具体的反例（攻击轨迹） - **UNKNOWN** — 求解器在限制范围内无法做出判定 - **VACUOUS** — （针对单个函数的标记）该函数的守卫不可满足，因此其证明是空洞的；请审查绑定配置 ## 开源核心 (MIT) CLI、翻译提示词、验证、可信 Z3 核心、Halmos 测试、基准绑定、DeFiHackLabs 语料库、DeFi 攻击运行器、ValuePacket 验证套件。商业层（独立）：托管 pipeline、CI 集成、仪表板、证明存储。 ## 路线图 - 集成 Kontrol 作为第二层字节码兜底机制 - 导出 CVL 以实现与 Certora Prover 的互操作 - 更丰富的 Z3 模型：复利 - 带有内联绑定审查的 VS Code 扩展 - 在 GitHub Pages 上发布公共排行榜

标签：MITM代理, 自定义脚本, 逆向工具