Skip to main content
Glama
Sign In
deenesjakoruzh
rei-checker

rei-checker

by fc0web
OverviewSchemaSourceRelated ServersDiscussionsAdmin
Python
Local

rei-checker-mcp

形式验证检查器 MCP v0.1.0a1 — 接收一行，返回真伪。不多也不少。

三值判定（VALID / INVALID / UNDECIDED）。判定路径中不涉及 LLM。每个 UNDECIDED 都带有原因代码，并记录在仅追加的反驳账本中。

许可证：AGPL-3.0-or-later 规范：CHECKER_SPEC_v0.md 设计不变量：CLAUDE.md

5 分钟运行

有 Python 3.9+ 就足够了。无外部依赖（仅标准库）。

git clone https://github.com/fc0web/rei-checker-mcp.git
cd rei-checker-mcp
python -m rei_checker verify "1 + 1 = 2"

预期输出：

{
  "verdict": "VALID",
  "elapsed_ms": 0,
  "checker_version": "rei-checker-mcp/0.1.0a1+spike-2026-08-22"
}

对于无法判定的输入，返回「无法判定」（spec §1.2）：

python -m rei_checker verify "some unknown thing"
{
  "verdict": "UNDECIDED",
  "elapsed_ms": 0,
  "checker_version": "rei-checker-mcp/0.1.0a1+spike-2026-08-22",
  "reason_code": "OUT_OF_SCOPE",
  "detail": "MockBackend has no rule for this expression"
}

退出码：0 = 决定性（VALID/INVALID），2 = UNDECIDED。可在 shell 脚本中直接根据「是否判定成功」进行分支。

Related MCP server: rei-verify

Ledger 累积与 stats

所有 verify 调用都会在 ledger.jsonl 中追加一行（spec §4）。

python -m rei_checker verify "1 + 1 = 2"
python -m rei_checker verify "1 + 1 = 3"
python -m rei_checker verify "<axiom-test>"
python -m rei_checker stats
{
  "total": 3,
  "valid": 1,
  "invalid": 1,
  "undecided": 1,
  "decision_rate": 0.6666666666666666,
  "reason_breakdown": {
    "MISSING_AXIOM": 1
  }
}

decision_rate 是唯一指标（spec §3）。初始值为 0.1 也没关系 — 达到可测量的状态 才是成功条件。

Ledger 的位置可通过 $REI_CHECKER_LEDGER 环境变量覆盖。默认 = 当前目录下的 ledger.jsonl。

作为 MCP server 使用

注册到 Claude Desktop：

{
  "mcpServers": {
    "rei-checker": {
      "command": "python",
      "args": ["-m", "rei_checker", "mcp"],
      "cwd": "C:/path/to/rei-checker-mcp",
      "env": {
        "REI_CHECKER_LEDGER": "C:/path/to/ledger.jsonl"
      }
    }
  }
}

MCP tool 只有 2 个（spec §2，刻意保持最小）：

  • verify(expression, context?, timeout_ms?) → { verdict, reason_code?, detail?, elapsed_ms, checker_version }

  • stats() → { total, valid, invalid, undecided, decision_rate, reason_breakdown }

哪些「尚未实现」（spec §2 明确）

以下为 v0 的非目标。如果试图实现，请 停下来确认：

  • UI / Web 前端

  • 用户注册・认证・计费

  • 游戏化、进度管理、学习记录

  • 自然语言对话・解说生成

  • 多后端支持（仅 Lean 4，v0 spike 使用 Mock backend 运行）

  • 对 Claude 特有功能的依赖

v0 的状态（诚实范围，2026-08-22 spike）

  • ✅ Schema（3 值 + 6 种 reason code）完全实现

  • ✅ Mock backend（测试用真值表 + 所有 reason code 触发）

  • ✅ Ledger（仅追加 JSONL、UTF-8、跳过格式错误的行）

  • ✅ stats() 聚合（decision_rate + reason_breakdown）

  • ✅ MCP stdio server（initialize + tools/list + tools/call）

  • ✅ CLI（verify / stats / mcp / version 子命令）

  • ⚠ Lean 4 backend 是 stub（v0.2 候选，计划在 lean_backend/ 目录实现）

  • ⚠ Timeout 执行是软性的（监控 elapsed，硬性进程终止在 v0.2）

「先被使用」优先（spec §1.3、§6.6）。Lean 4 harness 完成后，替换 backend 即可实际判定运行。API surface 不变。

Phase 2（v0 完成前不开始）

spec §9-13 定义的三层结构：

  • 第 1 层 checker（verify / stats）← v0，即本仓库

  • 第 2 层 education（locate_first_error / boundary_report / escalate）

  • 第 3 层 harness（calibration / regression / transfer）

实现顺序：第 1 层 → 第 3 层② calibration harness → 第 2 层。详见 spec §9-13。

测试

python -m unittest tests.test_all -v

按照 Spec §7，优先测试应返回 UNDECIDED 的情况（所有 reason_code 单独测试 + VALID/INVALID 正常路径）。

与 Rei stack 的关系（避免混淆）

本仓库刻意保持独立。与相邻工具的区别：

  • rei-verify（PyPI 0.1.0a1）= 反证机械 4 值判定，以 refutation-first 为主轴。本仓库为 3 值 verification-first，设计哲学不同。

  • grounded-check = LLM 输出的引用 grounding check，属于另一领域。

  • rei-preregister = 预测 SHA256 seal，事前注册工具。

  • discovery-worker = 反例 hunter，属于另一层。

由于集成违反 spec §5「多后端支持非目标」，目前不进行集成。

贡献 / 报告

请遵守 spec §8 的 4 项原则：

  1. 犹豫是否添加功能时，不添加

  2. 犹豫是否返回「大概正确」时，返回 UNDECIDED

  3. 犹豫是否将理论暴露到 API 时，不暴露

  4. 不着急，慢慢来

Issues: https://github.com/fc0web/rei-checker-mcp/issues

Available Tools

2 tools
statsA

Return aggregate stats from the refutation ledger. Includes decision_rate = (VALID + INVALID) / total, the sole metric of project success (spec §3), plus reason_breakdown that drives what the next sprint implements (spec §4).

NameRequiredDescriptionDefault

No parameters

TDQS

A4.2/5.0
Behavior4/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

No annotations, so description carries burden. It clearly states this is a read-style 'Return' operation with no side effects implied meetabst, and it specifies what data is included (decision_rate and reason_breakdown). It doesn't explicitly state it's non-destructive or need auth, but the context implies a read-only stats query. No contradictions.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

Two sentences, front-loaded with the purpose and two key outputs. Efficient.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness4/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

No output schema, so description explains the two things returnedches. It references spec sections, which is helpful. It's sufficient for the tool's simple scope, though it doesn't detail the exact breakdown structure. Minor gap.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

No parameters exist threre, so this dimension is trivially satisfied. The description explains what the output contains (decision_rate, reason_breakdown) which helps the agent understand what the tool will produce, but doesn't add parameter meaning since there are none.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose5/5

Does the description clearly state what the tool does and how it differs from similar tools?

Clear verb+resource: 'Return aggregate stats', specifies two concrete outputs (decision_rate and reason_breakdown) with explicit formulas, and references project specs. It distinguishes from the sole sibling 'verify' by being stats-focused, not per-item verification.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines4/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

Justifies use by linking decision_rate to 'sole metric of project success' and reason_breakdown to 'drives what the next sprint implements,' giving clear contexts for calling. It doesn't explicitly say when not to use or contrast with the sibling 'verify', but the purpose is specific enough that an agent can decide.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

verifyA

Verify one expression. Returns a three-valued verdict (VALID / INVALID / UNDECIDED) with a reason_code when UNDECIDED. No LLM anywhere on the judgment path (spec §1.1). The expression is normalized and recorded in the append-only refutation ledger (spec §4).

NameRequiredDescriptionDefault
contextNoOptional context (axioms, imports, prior definitions). Backend-defined semantics.
expressionYesThe expression to judge.
timeout_msNoHard timeout in milliseconds. Overrun → UNDECIDED/TIMEOUT. Default: 5000.

TDQS

A3.8/5.0
Behavior4/5

Does the description disclose side effects, auth requirements, rate limits, or destructive behavior?

With no annotations, the description carries the full behavioral burden. It discloses the three-valued return, conditional reason_code, the no-LLM guarantee, and the side effect of recording in an append-only refutation ledger. This is strong transparency, though it omits details like idempotency or error behavior.

Agents need to know what a tool does to the world before calling it. Descriptions should go beyond structured annotations to explain consequences.

Conciseness5/5

Is the description appropriately sized, front-loaded, and free of redundancy?

Three dense sentences with no filler. The verdict behavior is front-loaded, and the side-effect and no-LLM guarantees are stated efficiently. Every sentence earns its place.

Shorter descriptions cost fewer tokens and are easier for agents to parse. Every sentence should earn its place.

Completeness4/5

Given the tool's complexity, does the description cover enough for an agent to succeed on first attempt?

There is no output schema, but the description adequately explains return values and side effects. The input schema covers parameters. The only notable gap is the lack of explicit routing guidance relative to the sibling tool, but the core information needed to call and interpret the tool is present.

Complex tools with many parameters or behaviors need more documentation. Simple tools need less. This dimension scales expectations accordingly.

Parameters3/5

Does the description clarify parameter syntax, constraints, interactions, or defaults beyond what the schema provides?

Schema description coverage is 100%, so the schema already documents all three parameters. The description adds the fact that the expression is normalized, but it does not provide additional parameter-level guidance beyond what the schema already states.

Input schemas describe structure but not intent. Descriptions should explain non-obvious parameter relationships and valid value ranges.

Purpose4/5

Does the description clearly state what the tool does and how it differs from similar tools?

The description states a specific action ('Verify one expression') and clearly defines the output (VALID / INVALID / UNDECIDED with reason_code). It is easily distinguishable from the sibling 'stats' tool, though it does not explicitly name or contrast that sibling.

Agents choose between tools based on descriptions. A clear purpose with a specific verb and resource helps agents select the right tool.

Usage Guidelines3/5

Does the description explain when to use this tool, when not to, or what alternatives exist?

The description implies this tool is for judging a single expression, but it gives no explicit guidance on when to choose it over 'stats' or any other alternative. There are no stated exclusions or conditions, leaving the usage context to inference.

Agents often have multiple tools that could apply. Explicit usage guidance like "use X instead of Y when Z" prevents misuse.

Tool Schema Changelog

Recent tool additions, removals, and schema changes observed during successful MCP inspections.

  1. 2 tool updatesv0.1.0
    • First observedstats
    • First observedverify
Deploy Server
Shareable, User-Owned Context BackendPeople, applications, and agents read, write, and coordinate together in one context lake. Reach it over MCP, a CLI, a Python SDK, or REST.fulcradynamics.comAd

TDQS

A3.9/5.0

Scored across 2 tools

Disambiguation5/5

stats and verify are completely distinct: one provides aggregate metrics, the other checks individual expressions. There is no overlap in purpose, so an agent can easily select the correct tool.

Naming Consistency4/5

Both tool names are short, lowercase single words. While stats is a noun and verify is a verb, the naming style is consistent and clear, with no mixed conventions or confusing patterns.

Tool Count3/5

With only 2 tools, the server feels slightly thin, but the domain appears narrow (validation and ledger statistics). The count is borderline below the typical 3-15 range but not extreme enough to be a major issue.

Completeness4/5

The tools cover the core functions: verifying expressions and retrieving statistics. Missing operations like listing ledger entries or resetting data are not obvious gaps given the stated purpose, though a 'list' or 'detail' tool could be useful.

Maintenance

ActivityNo data
ResponsivenessSyncing

Resources

Related MCP Connectors

Related MCP Servers

  • rei-verify

    fc0web
    A
    license
    Not graded
    quality
    B
    maintenance
    A verification infrastructure and MCP server that specializes in refutation (negation) rather than generation, providing tools for counterexample search, Lean verification, and audit chains with a 4-value verdict system.
    MIT

  • decision-table

    tetracoralla
    A
    license
    Not graded
    quality
    A
    maintenance
    Provides deterministic decision and constraint evaluation for AI agents. Supports ruleset validation, fact evaluation, and constraint checking via MCP tools.
    Apache 2.0

  • certo

    jtraverso
    A
    license
    Not graded
    quality
    A
    maintenance
    Enables mathematical proof exploration and verification over MCP, where each result includes a certificate that can be checked independently without trusting the solver.
    40 PyPI
    1
    MIT