logic-lens：AI Agent 工具实践指南

如果把logic-lens放进候选清单，不能只看热度；它的定位是通过半正式执行跟踪进行逻辑优先 AI 代码审查（前提 → 跟踪 → 分歧 → 触发 → 补救措施），捕获 linter 遗漏的行为错误、类型契约违规和异步危险。团队若要把它用于软件开发，应先处理依赖、接口和异常处理往往比主路径更影响采用，否则试用结果很容易失真。与其反复读介绍，不如在隔离分支完成一个可回滚的小任务，再依据安装步骤、接口契约、测试结果和错误信息做取舍。对需要可检查开发流程而非单次演示的工程师来说，这个仓库值得继续验证；只求即装即用的人则要先看维护成本。

logic-lens

Logic-first 使用半正式执行的代码审查 tracing.

查找短绒、类型检查器和非结构化审查的行为错误 miss.

“使用结构化（半形式）推理的模型在代码语义任务上的准确率达到 87-93%，而对于非结构化思维链，准确率则为 76-78%，其中过程间错误的收益最大。” — Ugare 和 Chandra，代理代码推理（2026，arXiv：2603.01896）

没有痕迹的代码审查是一种猜测。标准审查可以发现风格问题和明显的错误。 Linters 捕获语法。但是，两者都没有捕获代码在孤立情况下看起来正确、通过所有测试，但仍然带来损坏的行为的错误类别——因为只有当两个函数以作者都没有预料到的方式交互时，才会出现错误。

logic-lens 强制 AI 在得出任何结论之前构建显式执行跟踪。每个发现都带有记录的前提 → 跟踪 → 分歧 → 触发 → 补救链，它准确地显示了审阅者如何得出发现的结果 - 而不仅仅是发现了什么。

九个逻辑风险

logic-lens 通过九个逻辑风险维度评估代码，其中六个维度源自代理代码推理 (L1–L6) 中的半形式推理方法，另外三个维度涵盖了超出本文单过程范围的现代危险 (L7–L9)：

它看起来像什么

鉴于此代码：

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 — 被调用者合约不匹配： get_discount 可能返回 None

前提： coupon_service.get_discount(code) 假设始终返回 0 到 1 之间的数字折扣率。 跟踪： discount_code 为真 → get_discount(discount_code) 被调用 → 结果赋给 discount → total * (1 - discount) 被评估。 分歧： get_discount 对于过期或无效代码（在其文档字符串中记录）返回 None。当discount为None时，1 - None升高TypeError。呼叫仅在快乐路径上到达db.save_order；错误的优惠券代码会中止该功能而不保存。 触发： process_order(1, [{'price': 10, 'qty': 1}], discount_code='EXPIRED2024') → TypeError: unsupported operand type(s) for -: 'int' and 'NoneType'；订单从未保存。 补救措施： 应用前检查 if discount is not None:。或者，让 get_discount 引发调用者可以显式处理的类型化异常 (InvalidCouponError)。

L3 — 边界盲点：空 items 列表

前提： items 假定包含至少一个元素。 跟踪： sum(item['price'] * item['qty'] for item in items) → 对于空列表返回 0 → total = 0 → order['total'] = 0 → 保存并确认。 分歧： 零商品订单会自动保存为 0.00 美元订单，并发送确认电子邮件。没有业务规则验证订单必须至少包含一项。 触发： process_order(1, []) → 预计会被拒绝；实际：订单保留为 total = 0 并发送确认电子邮件。 补救措施： 在总和前添加 if not items: raise ValueError("Order must contain at least one item")。这是一个业务不变量，而不是实现细节。

L8 — 资源生命周期危险：电子邮件故障时数据库连接未释放

前提： db.save_order 和 email_service.send_confirmation 假定均成功。 跟踪： db.save_order(order) 成功 → 连接保持打开状态 → email_service.send_confirmation(...) 引发 SMTPException → 函数通过未捕获的异常退出。 分歧： 数据库连接从未显式释放。根据 ORM 的连接池策略，这可能会在持续电子邮件失败的情况下耗尽池。 触发器：存根 email_service.send_confirmation 以引发 SMTPException，然后每个池槽调用一次 process_order - 池已耗尽，下一个调用在结账时阻塞。 补救措施： 将 email_service.send_confirmation 包装在 try/finally 块中，或将电子邮件发送分离到异步队列中，以便订单持久性不会与电子邮件传送耦合。

（+另外 2 个发现）

快速入门（60 秒）

克劳德代码用户：

/plugin marketplace add hyhmrright/logic-lens
/plugin install logic-lens@logic-lens-marketplace
/logic-review

然后粘贴任意函数。完毕。 （像 /logic-review 这样的简短命令会在第一次会话启动时自动安装。）

对于 Gemini CLI 和 Codex CLI，请参阅下面的 安装。

六大技能

logic-lens 提供六种技能：逻辑审查（通过执行跟踪查找行为错误）、逻辑解释（逐步跟踪代码实际执行的操作）、逻辑差异（验证两个版本在行为上等效）、逻辑定位（查找失败测试或崩溃的根本原因）、逻辑健康（跨代码库聚合逻辑运行状况仪表板）和逻辑修复全部（自主审核和修复管道） - 同意后，扫描目标，对每个发现应用修复，验证每个修复，并报告任何未解决的问题）。请参阅 用法 了解每个技能命令，并参阅 斜杠命令 了解平台特定的语法。

基准测试

logic-lens 针对 evals/content/v2/evals-v2.json 进行评分 — 104 个案例，跨越六个 技能，涵盖 12 种以上语言，案例以 Defects4J、QuixBugs、Therac-25 和 Ariane 5 查询，以及 Lu 等人的并发 bug 研究。每次跑步均由离线评分 基于规则的评分器（scripts/grade-iteration.py），而不是由 LLM 判断。

已发布的 logic-review 运行（36 例子集，claude-sonnet-4-6）：

每个冻结运行摘要都在 benchmarks/runs/ 中，由 benchmarks/index.json 编目，其中 benchmarks/reports/ 下的人类可读报告。复制其中任何一个 npm run content-evals.

如何读取这些数字。 评分者将每个案例分成逻辑子分数（是吗？ 找到错误并正确分类风险？）和 合约 子分数（报告是否 带有字面的铁法领域标签？）。 overall_pass_rate 混合两者，并签订合约 断言约占总数的 25%——因此总体而言是综合记录，而不是纯粹的衡量标准 推理质量。请参阅 benchmarks/README.md 了解指标层次结构和多重运行 平均规则（已观察到单次运行案例级增量波动 ±25pp）。

这里没有测量什么。 没有公开与无人协助的克劳德的正面交锋 这个回购协议；上面的版本号是诚实的声明。结果还取决于 很大程度上取决于实际调用该技能的主机模型 - 请参阅 docs/MODEL_COMPATIBILITY.md，其中俳句处于 claude -p 模式 得分38.7%几乎完全是因为它直接回答而不加载技能。

比较如何

~ = 偶尔/不一致

logic-lens 不会取代您的 linter。 它可以捕获 linter 无法捕获的内容：被调用者契约违规、状态突变危险和控制流逃逸 - 这些错误会在语法干净、lint 传递的代码中导致生产事件。

安装

克劳德代码（推荐）

已运行快速入门？您已完成 — 跳至 斜线命令。

通过插件市场

/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/

双子座 CLI

通过扩展

/extensions install https://github.com/hyhmrright/logic-lens

手动安装

mkdir -p ~/.gemini/skills/logic-lens
cp -r skills/* ~/.gemini/skills/logic-lens/

法典 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。简短形式 通过会话启动挂钩在第一个会话启动时自动安装（macOS、Linux 和 Windows 通过 WSL / Git Bash）。
• Codex CLI：在 Codex 会话中输入 $logic-* — 这些不是 shell 命令。

用途

调用语法位于上面的 斜杠命令 中。每项技能对您的输入有何作用：

logic-review — 代码逻辑审查

粘贴代码或将 AI 指向该文件。 logic-lens 为每个可疑路径构建显式执行跟踪，并仅报告具有记录的前提 → 跟踪 → 分歧 → 触发器 → 补救链的发现结果。

logic-explain — 执行说明

问“这段代码实际上做了什么？”并获得跨越函数边界的逐步跟踪，而不是代码似乎执行的操作的自然语言摘要。

logic-diff — 语义差异

粘贴函数的两个版本。 logic-lens 会跟踪两者并报告它们在行为上是否相同，如果不同，则准确报告哪个执行路径会产生不同的结果。

logic-locate — 故障定位

将失败的测试、堆栈跟踪或错误报告与相关代码一起粘贴。 logic-lens 从未能识别确切的分歧点开始向后追溯——区分根本原因和症状。

logic-health — 逻辑健康仪表板

在代码库中运行简短的逻辑审查，并生成按风险维度细分的加权逻辑健康评分 (0-100)。在发布之前、审核期间或进入不熟悉的代码库时使用。

logic-fix-all — 自主审核和修复

将其指向目录或文件。 logic-lens 首先请求同意，因为此模式需要大量令牌并编辑文件。同意后，它会扫描范围，收集每个严重级别（L1-L9）的结果，按优先级顺序应用修复，使用语义差异验证每个修复，并重新确认代码库是干净的，除非它达到配置的迭代上限或需要设计决策。最终输出是一个修复日志表，列出了所做的每个更改及其验证状态。

配置

将 .logic-lens.yaml 放入项目根目录中以自定义行为：

# Skip concurrency checks in confirmed single-threaded code
disable:
  - L7

# Treat all boundary issues as critical for this safety-critical module
severity:
  L3: critical

# Exclude generated files and vendor code from analysis
ignore:
  - "tests/fixtures/**"
  - "vendor/**"
  - "**/*.generated.*"

所有设置都是可选的 - 完全省略该文件以实现默认行为。

语言支持

logic-lens 与语言无关。半形式推理方法适用于任何可以通过阅读源代码来跟踪名称解析、类型契约和执行路径的语言。共享指南包括以下语言特定的跟踪注释：

Python · JavaScript / TypeScript · Java / Kotlin · Go · Rust · SQL

其他语言使用通用方法——作用域链规则、类型强制行为和异常传播语义是唯一需要的特定于语言的知识。

它是如何运作的

logic-lens 不执行代码或使用静态分析工具。它的工作原理是提示 AI 遵循结构化推理模板，该模板反映了代理代码推理（Ugare 和 Chandra，2026）中的半正式方法。

该论文的关键见解是：当模型在跟踪之前被迫明确陈述前提时，它们会以 87-93% 的准确率捕获过程间错误。如果没有这种结构，相同的模型在 22% 到 24% 的情况下会错过这些错误，因为它们会根据代码外观进行模式匹配，而不是通过执行进行推理。

根据调查结果执行的纪律：

1. 前提 — 陈述有关名称解析、类型和先决条件的每个假设
2. Trace — 一步步遵循实际执行路径，跨越函数边界
3. 分歧 — 确定前提破裂的确切点以及接下来发生的情况
4. 触发器 — 提供可重现它的具体输入，足够具体以粘贴到 REPL 中
5. 补救措施 - 制定解决方案来解决分歧，而不仅仅是其症状

在前提 → 跟踪 → 分歧完成之前，不得写入触发器或补救措施。这是 逻辑镜头的铁律。 （关键和警告结果需要触发，可选 寻求建议。）

项目结构

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 (104 cases — the benchmark suite)
│   ├── trigger/v2/trigger-evals-*.json  # Per-skill trigger eval sets (6 × 20 cases)
│   ├── real-world/               # Real-code probes — second verification line, incl. decoys
│   └── v1/                       # Legacy v1 cases, archived
├── benchmarks/
│   ├── index.json                # Catalog of published runs
│   ├── runs/                     # Frozen run summaries (JSON)
│   └── reports/                  # Human-readable reports, per version tag
├── scripts/                      # Dev utilities (validate, run-content-evals, grade-iteration)
├── tests/                        # Python unit tests for the grader
├── docs/                         # Model compatibility, research references, case studies
└── CONTRIBUTING.md

为什么要进行半形式推理？

AI- 辅助开发使代码库的增长速度超过了人工审核能力。漏掉的错误越来越多地是过程间的类型——这些错误需要同时牢记两个函数的契约并注意它们何时不匹配。

“无论分配多少女性，生孩子都需要九个月的时间。” ——弗雷德里克·布鲁克斯，《人月神话》（1975）

如果添加 AI 审阅者并不能解决问题，如果他们犯了与人类审阅者相同的推理错误：表面外观上的模式匹配、锚定在快乐的路径上、当代码“看起来不错”时跳过跟踪。 logic-lens 在方法论层面解决了这个问题——不是通过提示 AI“更加小心”，而是通过构建推理过程，使其无法跳过错误隐藏的步骤。已发布的基准摘要位于 benchmarks/runs/ 中。

传播信息

如果 logic-lens 使您免于生产事故，请让其他人知道！

• 在 X (Twitter) 上分享：点击发推文
• 添加徽章：通过将此徽章添加到您的 README 来显示您的存储库经过逻辑审查：

阅读

• 为什么 AI 代码审查会错过逻辑错误 - 以及结构化执行跟踪如何修复它 - DEV.to 深入探讨逻辑镜头背后的方法