KryptosAI/counterflow-action
GitHub: KryptosAI/counterflow-action
基于 Z3 求解器的 Solidity 智能合约不变式验证 GitHub Action，在 CI 中自动证明合约安全性或输出具体反例。
Stars: 0 | Forks: 0
# Counterflow 动作
为 Solidity 和 DeFi 智能合约提供基于 Z3 证明的确定性不变式检查。
给定一个已审查的 **binding**（结构化规范），Counterflow 要么证明你的不变式对**所有**输入成立，要么在任务失败时提供一个具体的反例。
## 用法
```
- uses: KryptosAI/counterflow-action@v1
with:
binding: path/to/Contract.binding.json
```
就这样。该步骤在 **PROVED** 时显示为绿色，在 **VIOLATED**（退出码 3）或求解器错误（退出码 2）时显示为红色。判定报告将始终写入到任务摘要中。
## 完整示例
```
name: verify
on: [push, pull_request]
jobs:
counterflow:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- uses: KryptosAI/counterflow-action@v1
with:
binding: examples/TokenPool.binding.json
```
## 输入
| 输入 | 必需 | 默认值 | 描述 |
|---|---|---|---|
| `binding` | 是 | — | 已审查的 binding JSON 的路径 |
| `version` | 否 | `latest` | `@kryptosai/counterflow` 的 npm 版本 |
| `github-token` | 否 | `''` | 设置为 `${{ secrets.GITHUB_TOKEN }}` 以获取带有判定结果的 PR 评论（重新运行时会原地更新） |
## 输出
| 输出 | 描述 |
|---|---|
| `verdict` | `proved` \| `violated` \| `unknown` \| `error` |
## PR 评论
```
- uses: KryptosAI/counterflow-action@v1
with:
binding: examples/TokenPool.binding.json
github-token: ${{ secrets.GITHUB_TOKEN }}
```
该 action 会在每个 PR 下发布一条评论，并在后续运行中对其进行更新。
## 判定结果的含义
- **PROVED** — 建模的转换在所有输入情况下都能保持每个不变式成立（基于已审查 binding 的归纳证明）
- **VIOLATED** — Z3 找到了一个具体的反例（漏洞利用追踪）；该步骤失败
- **UNKNOWN** — 求解器在限制范围内无法做出判定
## 链接
- [GitHub 上的 Counterflow](https://github.com/KryptosAI/counterflow) — CLI、文档、基准测试套件
- [npm 上的 @kryptosai/counterflow](https://www.npmjs.com/package/@kryptosai/counterflow)
- [实时验证排行榜](https://kryptosai.github.io/counterflow/)
## 许可证
MIT — 查看 [LICENSE](LICENSE)。
标签：LNA, MITM代理, 暗色界面