hyhmrright/logic-lens

GitHub: hyhmrright/logic-lens

一款基于半形式化执行追踪的AI代码审查技能,通过强制大模型构建结构化推理链,精准捕获传统Lint和普通审查遗漏的深层跨过程行为漏洞。

Stars: 3 | Forks: 0

Logic-Lens

以逻辑为先的代码审查,采用半形式化执行追踪。
能够发现 linter、类型检查器和非结构化审查遗漏的行为漏洞。

九大风险示例六大技能基准测试安装说明使用方法配置贡献指南

Version MIT License Claude Code Plugin Codex CLI Skill Gemini CLI Extension Verified 58/58

GitHub Stars GitHub Forks Issues Pull Requests Latest Release Last commit

**没有执行追踪的代码审查只是猜测。** 标准审查能发现样式问题和明显错误。Linters 能捕获语法错误。但是,当代码单独看起来是正确的,通过了所有测试,却依然带着残缺的行为发布时,这两者都无法捕获这类漏洞——因为该漏洞仅在两个函数以双方作者都未曾预料到的方式交互时才会出现。 **Logic-Lens 强制 AI 在得出任何结论之前构建一个显式的执行追踪**。每项发现都附带一个记录在案的“前提 → 追踪 → 偏差 → 补救”链,准确展示审查者是如何得出该发现的——而不仅仅是展示了发现了什么。 ## 九大逻辑风险 Logic-Lens 跨 **九个逻辑风险维度** 评估代码——其中六个源自《*Agentic Code Reasoning*》中的半形式化推理方法(L1–L6),另外三个则涵盖了该论文单进程范围之外的新型隐患(L7–L9): | 代码 | 风险 | 捕获内容 | |------|------|----------------| | 🔀 **L1** | Shadow Override (同名覆盖) | 名称解析到了与预期不同的定义——变量遮蔽、导入别名、继承覆盖 | | 📐 **L2** | Type Contract Breach (类型契约破坏) | 函数接收到无法正确处理的类型,通常通过隐式强制转换或条件路径传入 | | 🔲 **L3** | Boundary Blindspot (边界盲点) | 未被追踪的边缘情况:null、空值、零值、最大/最小边界、单元素序列 | | ⚠️ **L4** | State Mutation Hazard (状态突变风险) | 单个执行路径上的顺序别名或迭代期间突变隐患 | | 🚪 **L5** | Control Flow Escape (控制流逃逸) | 提前退出跳过了必要的非生命周期操作——状态更新、验证、审计事件、通知 | | 🔗 **L6** | Callee Contract Mismatch (被调用方契约不匹配) | 调用代码假定了返回值语义、异常行为或幂等性,但被调用方并未提供保证 | | 🧵 **L7** | Concurrency / Async Hazard (并发/异步风险) | 跨越 `await` / 锁 / channel 边界的竞态;双重获取;取消后发送;缺失 happens-before 关系 | | 🔁 **L8** | Resource Lifecycle Hazard (资源生命周期风险) | 获取/释放不平衡——缺失释放路径、双重释放、所有权转移但未更新释放计划 | | 🕒 **L9** | Time / Locale Hazard (时间/区域设置风险) | 朴素类型与时区敏感型 datetime、DST 跳变、区域敏感的排序/大小写、编码往返转换、小数点分隔符偏移 | ## 效果展示 给定以下代码: ``` def process_order(order_id, items, discount_code=None): order = db.get_order(order_id) total = sum(item['price'] * item['qty'] for item in items) if discount_code: discount = coupon_service.get_discount(discount_code) total = total * (1 - discount) order['total'] = total order['items'] = items db.save_order(order) email_service.send_confirmation(order['email'], total) ``` Logic-Lens 输出结果如下: **逻辑健康度:31/100** *此函数包含一个被调用方契约不匹配问题,会导致静默的除零风险;一个针对空项目列表的边界盲点;以及一个资源生命周期风险,即在电子邮件发送失败时会泄漏数据库连接。* ### 🔴 L6 — Callee Contract Mismatch: `get_discount` 可能返回 `None` **前提:** 假定 `coupon_service.get_discount(code)` 总是返回一个介于 0 和 1 之间的数值折扣率。 **追踪:** `discount_code` 为真值 → 调用 `get_discount(discount_code)` → 将结果赋值给 `discount` → 计算 `total * (1 - discount)`。 **偏差:** 对于过期或无效的 code,`get_discount` 返回 `None`(记录在其 docstring 中)。当 `discount` 为 `None` 时,`1 - None` 会引发 `TypeError`。该调用仅在正常路径上执行到 `db.save_order`;无效的优惠券 code 会中断函数执行且不进行保存。 **补救:** 在应用折扣之前检查 `if discount is not None:`。或者,让 `get_discount` 引发一个类型化的异常(`InvalidCouponError`),以便调用方能够显式处理。 ### 🔴 L3 — Boundary Blindspot: 空的 `items` 列表 **前提:** 假定 `items` 包含至少一个元素。 **追踪:** `sum(item['price'] * item['qty'] for item in items)` → 对空列表返回 `0` → `total = 0` → `order['total'] = 0` → 被保存并确认。 **偏差:** 包含零个项目的订单会被静默保存为 $0.00 的订单,并会发送确认电子邮件。没有业务规则验证订单必须至少包含一个项目。 **补救:** 在求和前添加 `if not items: raise ValueError("Order must contain at least one item")`。这是一个业务不变量,而不是实现细节。 ### 🟡 L8 — Resource Lifecycle Hazard: 电子邮件发送失败时数据库连接未释放 **前提:** 假定 `db.save_order` 和 `email_service.send_confirmation` 都会成功执行。 **追踪:** `db.save_order(order)` 成功 → 保持连接打开 → `email_service.send_confirmation(...)` 引发 `SMTPException` → 函数通过未捕获的异常退出。 **偏差:** 数据库连接从未被显式释放。根据 ORM 的连接池策略,在持续的电子邮件发送失败期间,这可能会耗尽连接池。 **补救:** 将 `email_service.send_confirmation` 封装在 `try/finally` 块中,或者将电子邮件发送分离到异步队列中,从而解耦订单持久化与邮件投递的依赖。 *(+ 另外 2 项发现)* ## 快速开始 (60 秒) **Claude Code 用户:** ``` /plugin marketplace add hyhmrright/logic-lens /plugin install logic-lens@logic-lens-marketplace /logic-review ``` 然后粘贴任意函数。完成。*(如 `/logic-review` 等简短命令会在首次会话启动时自动安装。)* 对于 Gemini CLI 和 Codex CLI,请参阅下方的 [安装说明](#installation)。 ## 六大技能 Logic-Lens 提供六项技能:**logic-review**(通过执行追踪发现行为漏洞)、**logic-explain**(逐步追踪代码的实际运行情况)、**logic-diff**(验证两个版本在行为上是否等效)、**logic-locate**(定位失败测试或崩溃的根本原因)、**logic-health**(跨代码库生成聚合的逻辑健康度仪表盘)以及 **logic-fix-all**(自主审计与修复流水线——在获得同意后,扫描目标代码,为每项发现应用修复,验证每一项修复,并报告任何未解决的问题)。有关各项技能的命令,请参阅 [使用方法](#usage);有关特定平台的语法,请参阅 [斜杠命令](#slash-commands)。 ## 基准测试 在 3 个真实漏洞场景(跨过程、边界、状态突变)中进行了测试: | 标准 | Logic-Lens | 单独使用 Claude | |-----------|:----------:|:------------:| | 在得出发现之前陈述了显式前提 | ✅ 100% | ❌ 0% | | 提供了逐步的执行追踪 | ✅ 100% | ❌ 0% | | 识别出了确切的偏差点 | ✅ 100% | ❌ 0% | | 为每项发现标记了风险代码 (L1–L9) | ✅ 100% | ❌ 0% | | 检测跨过程漏洞 | ✅ 100% | ✅ 68% | | 检测边界盲点 | ✅ 100% | ✅ 71% | | **总体通过率** | **91%** | **19%** | 差距并不在于 Claude *能够*发现什么——而在于它*始终一致地*发现了什么,并且每次都提供了一个展示其推理过程的可追踪推理链。 ## 对比分析 | | Logic-Lens | ESLint / Pylint | GitHub Copilot Review | 纯 Claude | |---|:---:|:---:|:---:|:---:| | 检测语法和样式问题 | — | ✅ | ✅ | ~ | | 每项发现均提供显式执行追踪 | ✅ | ❌ | ❌ | ❌ | | 前提 → 追踪 → 偏差 → 补救 | ✅ | ❌ | ❌ | ❌ | | 带有一致严重性标签的发现 | ✅ | ✅ | ~ | ❌ | | 跨过程漏洞检测 | ✅ | ❌ | ~ | ~ | | 边界与 null 路径分析 | ✅ | ~ | ~ | ~ | | 零配置,适用于任何语言 | ✅ | ❌ | ✅ | ✅ | | 推理过程可审计/可复现 | ✅ | ✅ | ❌ | ❌ | **Logic-Lens 并不能替代你的 linter。** 它能捕获 linter 无法检测到的内容:被调用方契约破坏、状态突变风险和控制流逃逸——这些正是导致语法正确且通过 lint 的代码发生生产事故的元凶。 ## 安装说明 ### Claude Code (推荐) *已经运行过快速开始了?你已经完成了——跳转至 [斜杠命令](#slash-commands)。* #### 通过插件市场 ``` /plugin marketplace add hyhmrright/logic-lens /plugin install logic-lens@logic-lens-marketplace ``` 短命令(如 `/logic-review`)会在首次会话启动时自动安装。要手动安装: ``` cp commands/*.md ~/.claude/commands/ ``` #### 手动安装 ``` mkdir -p ~/.claude/skills/logic-lens cp -r skills/* ~/.claude/skills/logic-lens/ ``` ### Gemini CLI #### 通过扩展 ``` /extensions install https://github.com/hyhmrright/logic-lens ``` #### 手动安装 ``` mkdir -p ~/.gemini/skills/logic-lens cp -r skills/* ~/.gemini/skills/logic-lens/ ``` ### Codex CLI #### 通过技能安装器 (在 Codex 会话中) ``` Install the logic-lens skill from hyhmrright/logic-lens ``` #### 命令行 ``` python3 ~/.codex/skills/.system/skill-installer/scripts/install-skill-from-github.py \ --repo hyhmrright/logic-lens --path skills --name logic-lens ``` #### 手动安装 ``` git clone https://github.com/hyhmrright/logic-lens.git /tmp/logic-lens mkdir -p ~/.codex/skills/logic-lens cp -r /tmp/logic-lens/skills/* ~/.codex/skills/logic-lens/ ``` ## 斜杠命令 ### Claude Code | 命令 | 简写形式 | 动作 | |---------|------------|--------| | `/logic-lens:logic-review` | `/logic-review` | 通过执行追踪进行代码逻辑审查 | | `/logic-lens:logic-explain` | `/logic-explain` | 逐步的执行解释 | | `/logic-lens:logic-diff` | `/logic-diff` | 检查两个版本之间的语义等价性 | | `/logic-lens:logic-locate` | `/logic-locate` | 失败测试或崩溃的根本原因定位 | | `/logic-lens:logic-health` | `/logic-health` | 代码库的聚合逻辑健康度仪表盘 | | `/logic-lens:logic-fix-all` | `/logic-fix-all` | 自主的审计与修复流水线——询问同意,然后修复并验证逻辑问题 | ### Gemini CLI | 命令 | 动作 | |---------|--------| | `/logic-review` | 通过执行追踪进行代码逻辑审查 | | `/logic-explain` | 逐步的执行解释 | | `/logic-diff` | 检查两个版本之间的语义等价性 | | `/logic-locate` | 失败测试或崩溃的根本原因定位 | | `/logic-health` | 代码库的聚合逻辑健康度仪表盘 | | `/logic-fix-all` | 自主的审计与修复流水线——询问同意,然后修复并验证逻辑问题 | ### Codex CLI | 命令 | 动作 | |---------|--------| | `$logic-review` | 通过执行追踪进行代码逻辑审查 | | `$logic-explain` | 逐步的执行解释 | | `$logic-diff` | 检查两个版本之间的语义等价性 | | `$logic-locate` | 失败测试或崩溃的根本原因定位 | | `$logic-health` | 代码库的聚合逻辑健康度仪表盘 | | `$logic-fix-all` | 自主的审计与修复流水线——询问同意,然后修复并验证逻辑问题 | 请在 Codex 会话中输入这些 `$logic-*` 调用;它们不是 Shell 命令。 ## 使用方法 ### 代码逻辑审查 ``` /logic-review # Claude Code (short form) / Gemini CLI /logic-lens:logic-review # Claude Code (full form) $logic-review # Codex CLI ``` 粘贴代码或让 AI 指向该文件。Logic-Lens 会为每个可疑路径构建显式的执行追踪,并且仅报告附带“前提 → 追踪 → 偏差 → 补救”链的发现。 ### 执行解释 ``` /logic-explain # Claude Code (short form) / Gemini CLI /logic-lens:logic-explain # Claude Code (full form) $logic-explain # Codex CLI ``` 询问“这段代码实际上做了什么?”,您将获得一个跨越函数边界的逐步追踪结果,而不是一段对代码功能的自然语言总结。 ### 语义 Diff ``` /logic-diff # Claude Code (short form) / Gemini CLI /logic-lens:logic-diff # Claude Code (full form) $logic-diff # Codex CLI ``` 粘贴一个函数的两个版本。Logic-Lens 会对两者进行追踪,并报告它们在行为上是否等效——如果不等效,会准确指出是哪条执行路径产生了不同的结果。 ### 故障定位 ``` /logic-locate # Claude Code (short form) / Gemini CLI /logic-lens:logic-locate # Claude Code (full form) $logic-locate # Codex CLI ``` 将失败的测试、堆栈跟踪或 Bug 报告连同相关代码一起粘贴进去。Logic-Lens 会从失败处向后追踪,以识别确切的偏差点——区分根本原因与表象症状。 ### 逻辑健康度仪表盘 ``` /logic-health # Claude Code (short form) / Gemini CLI /logic-lens:logic-health # Claude Code (full form) $logic-health # Codex CLI ``` 跨代码库运行简略的逻辑审查,并生成一个按风险维度细分的加权逻辑健康度评分(0–100)。可在发布前、审计期间或在接手不熟悉的代码库时使用。 ### 自主的审计与修复 ``` /logic-fix-all # Claude Code (short form) / Gemini CLI /logic-lens:logic-fix-all # Claude Code (full form) $logic-fix-all # Codex CLI ``` 将其指向一个目录或文件。Logic-Lens 首先会征求您的同意,因为此模式会消耗较多 token 并会编辑文件。获得同意后,它会扫描范围,收集每个严重级别(L1–L9)的发现,按优先级顺序应用修复,通过语义 Diff 验证每项修复,并在遇到配置的迭代上限或需要设计决策之前,重新确认代码库是干净的。最终输出是一个修复日志表,列出了所做的每一项更改及其验证状态。 ## 配置 在项目根目录下放置一个 `.logic-lens.yaml` 文件以自定义行为: ``` # 在已确认的单线程代码中跳过并发检查 disable: - L7 # 将所有边界问题视为此安全关键模块的关键问题 severity: L3: critical # 从分析中排除生成文件和 vendor code ignore: - "tests/fixtures/**" - "vendor/**" - "**/*.generated.*" ``` | 设置项 | 描述 | |---------|-------------| | `disable` | 要跳过的风险代码(`L1`–`L9`,或自定义的 `C1`, `C2`, ...) | | `severity` | 覆盖严重性层级(`critical` / `warning` / `suggestion`) | | `ignore` | 用于排除分析文件的 Glob 模式 | | `focus` | 仅评估这些风险代码 | | `custom_risks` | 定义项目特定的风险代码(`C1`, `C2`, ...),包含 `code`、`name`、`description`、`severity` | 所有设置都是可选的——完全省略该文件即可使用默认行为。 ## 语言支持 Logic-Lens 是语言无关的。这种半形式化推理方法适用于任何可以通过阅读源代码来追踪名称解析、类型契约和执行路径的语言。共享指南中包含以下语言特定的追踪注意事项: **Python** · **JavaScript / TypeScript** · **Java / Kotlin** · **Go** · **Rust** · **SQL** 其他语言也可以使用通用方法——作用域链规则、类型强制转换行为和异常传播语义是唯一需要的语言特定知识。 ## 工作原理 Logic-Lens 不执行代码,也不使用静态分析工具。它通过提示 AI 遵循一个结构化的推理模板来工作,该模板反映了《*Agentic Code Reasoning*》(Ugare & Chandra, 2026)中的半形式化方法。 该论文的关键见解是:当模型被强制在追踪前显式陈述其前提时,它们能以 87%–93% 的准确率捕获跨过程漏洞。如果没有这种结构,相同的模型会在 22%–24% 的情况下漏掉这些漏洞——因为它们是在对代码外观进行模式匹配,而不是对执行过程进行推理。 每项发现强制执行的规范: 1. **前提** —— 陈述关于名称解析、类型和前置条件的每一项假设 2. **追踪** —— 逐步遵循实际的执行路径,跨越函数边界 3. **偏差** —— 识别前提崩溃的确切位置及其后续影响 4. **补救** —— 开出解决偏差本身(而不仅是其表象症状)的修复处方 如果没有这四个部分,就不会报告任何发现。这就是 Logic-Lens 的**铁律**。 ## 项目结构 ``` logic-lens/ ├── .claude-plugin/ # Claude Code plugin metadata ├── .codex-plugin/ # Codex CLI plugin metadata ├── gemini-extension.json # Gemini CLI extension metadata ├── skills/ │ ├── _shared/ # Shared framework files │ │ ├── common.md # Language rule, Iron Law, Logic Score, yaml schema │ │ ├── logic-risks.md # L1–L9 risk taxonomy with examples │ │ ├── semiformal-guide.md # Execution tracing methodology + min thresholds │ │ ├── semiformal-checklist.md # Premises Construction Checklist (single source) │ │ └── report-template.md # Report Template (English + Chinese, single source) │ ├── logic-review/ # Skill 1: Code logic review │ ├── logic-explain/ # Skill 2: Execution explanation │ ├── logic-diff/ # Skill 3: Semantic diff │ ├── logic-locate/ # Skill 4: Fault localization │ ├── logic-health/ # Skill 5: Health dashboard │ └── logic-fix-all/ # Skill 6: Autonomous audit-and-fix │ ├── SKILL.md │ ├── logic-fix-all-guide.md # Navigation + shared context │ ├── guide-phases-0-2-consent-scope-health.md │ ├── guide-phases-3-5-review-locate-clarify.md │ └── guide-phases-6-9-fix-iterate-report.md ├── commands/ # Short-form command wrappers (auto-installed by hook) ├── hooks/ # Session-start hook ├── evals/ │ ├── content/v2/evals-v2.json # Content eval cases (current benchmark suite) │ └── trigger/v2/trigger-evals-*.json # Per-skill trigger eval sets (6 × 20 cases) ├── benchmarks/runs/ # Frozen published benchmark summaries ├── scripts/ # Dev utilities (validate, run-content-evals, grade-iteration) └── CONTRIBUTING.md ``` ## 为什么选择半形式化推理? AI 辅助开发正在让代码库的增长速度超过人类审查的承载能力。漏网之鱼越来越多地变成了跨过程类型——这类漏洞需要同时铭记两个函数的契约,并在它们不匹配时察觉到问题。 如果 AI 审查员犯了与人类审查员相同的推理错误,那么添加 AI 审查员并不能解决问题:他们依然在表面外观上进行模式匹配,锚定在正常执行路径(Happy Path)上,并在代码“看起来没问题”时跳过追踪步骤。Logic-Lens 在方法论层面解决了这个问题——它不是通过提示 AI “更加小心”,而是通过结构化推理过程,使其无法跳过漏洞隐藏的那个步骤。已发布的基准测试摘要位于 `benchmarks/runs/` 中。 ## 贡献指南 请参阅 [CONTRIBUTING.md](CONTRIBUTING.md)。Logic-Lens 专为通用场景设计——提交的贡献不得嵌入有关特定语言、框架或开发工作流的假设。 目前最好的贡献方式是新的评估测试用例,特别是源自真实生产事故的跨过程漏洞。有关格式请参阅 [CONTRIBUTING.md](CONTRIBUTING.md)。 **刚接触本项目?最快的贡献方式是提交新的评估测试用例——请参阅 [issue 模板](https://github.com/hyhmrright/logic-lens/issues/new?template=eval-contribution.md)。** ## 许可证 ## 延伸阅读 - [为什么 AI 代码审查会遗漏逻辑漏洞——以及结构化执行追踪如何修复它们](https://dev.to/hyhmrright/why-ai-code-review-misses-logic-bugs-and-how-structured-execution-tracing-fixes-it-3n0p) — DEV.to 上关于 logic-lens 背后方法的深入探讨 - - MIT 许可证 — 详情请参阅 [LICENSE](LICENSE)。 ## 致谢 Logic-Lens 基于以下研究: - Ugare & Chandra — *Agentic Code Reasoning* (2026, arXiv:2603.01896) 本项目中引用的半形式化推理方法、风险分类体系和准确性基准测试均源自该研究或受其启发。

⭐ 如果 Logic-Lens 帮助你在发布前拦截了一个漏洞,请为其点亮星标!

## Star 历史 [![Star History Chart](https://api.star-history.com/svg?repos=hyhmrright/logic-lens&type=Date)](https://star-history.com/#hyhmrright/logic-lens&Date)
标签:AI代码审查, Claude Code, Codex CLI, DLL 劫持, Gemini CLI, Linting, TLS抓取, 代码逻辑分析, 半形式化执行追踪, 大语言模型, 威胁情报, 开发者工具, 异步风险检测, 插件, 类型契约, 行为漏洞检测, 软件安全, 错误基检测, 静态代码分析