rei-verify

Refutation Machine — A verification infrastructure and MCP server specializing in negation, not generation.

Version: 0.1.0a1 (2026-08-19) — 4 primitives + 4 refutation tools + 8 MCP tools + integration demo. Tests: 198/0 PASS.

Why a "Refutation Machine"?

Generation saturates. Refutation does not.

Current LLMs are fluent. They can output plausible proof outlines, plausible code, plausible theorem names, independent of whether they are true.

Even if benchmarks saturate at 96%, this structure doesn't change. What the world lacks is not a "machine that creates plausible things," but rather a "machine that reliably kills plausible things."

The core promise of the refutation machine:

• Upon receiving a claim, allocate computational resources to counterexample search. Proof attempts are deferred.

• If no counterexample is found, explicitly return "the shape of the search space in which nothing was found" (don't disguise silence as success).

• The output always includes "the place where the claim would break if it were false." Lean 4's zero sorry is the strictest special case of this.

• Treat "could not be refuted" and "correct" as distinct at the type level.

Related MCP server: prova-mcp

4-value verdict (core discipline: "never lie")

class Verdict(str, Enum):
    CONFIRMED = "confirmed"           # post-condition PASS + marker 空
    REFUTED = "refuted"               # 具体的な counter-witness が 得られた
    HOLDING = "holding"               # counter-witness 未発見 かつ marker 非空
    INCOMPLETE_FRAME = "incomplete_frame"  # 主張自体が well-formed でない

Not binary TRUE/FALSE = not refuted ≠ correct. Typing of a 12-year IUT holding discipline.

Type-level guarantee: "Don't disguise silence as success": All verdicts other than CONFIRMED require at least one IncompleteMarker (dimension + what_was_tried + what_was_not_tried + reason) (dataclass invariant, unbreakable).

4 primitives (rei_verify)

4 refutation tools (rei_verify.*)

The heart of the refutation machine. All tools return a consistent shape: VerdictWithMarkers (4-value verdict + markers + audit_hashes).

★ Only refute_lean_source can return CONFIRMED (only cases where the Lean 4 kernel certifies sorry-free). The other three tools always return REFUTED or HOLDING = type-level guarantee of the "absence of counter-example is not proof" discipline.

8 MCP tools

Can be called directly from LLM clients such as Claude Desktop, Cursor, Cline:

MCP-safe expressions use restricted eval: pre-reject __import__ / exec / eval / open / __ prefix, only allow whitelist _SAFE_BUILTINS (abs/min/max/sum/len/int/float/str/bool/round/any/all/range).

Installation

pip install rei-verify           # core primitives (no external deps)
pip install rei-verify[mcp]      # + MCP server

or from source:

git clone https://github.com/fc0web/rei-verify.git
cd rei-verify
pip install -e .[mcp]

Requires Python 3.10+ (dataclass + Enum + typing new features). Core primitives work with only the standard library (import OK even without mcp package).

Usage — library

VerifiedExecution (custom)

from pathlib import Path
from rei_verify import (
    Verdict, IncompleteMarker, PostCheckResult,
    VerifiedExecution, AuditChain,
)

audit = AuditChain(Path("./reasoning.jsonl"))
ve = VerifiedExecution(
    claim="1 + 1 == 2",
    pre_check=lambda: True,
    post_check=lambda r: PostCheckResult(refuted=(r != 2), markers=[]),
    audit=audit,
)
result = ve.run(lambda: 1 + 1)
# result.verdict == Verdict.CONFIRMED
# result.audit_hashes == [h1, h2, h3, h4, h5]  # 5 phase entry

refute_lean_source

from rei_verify.refute import refute_lean_source

result = refute_lean_source(
    claim="trivial True holds",
    lean_source="theorem trivial_true : True := trivial\n",
    audit=audit,
    theorem_name="trivial_true",
    timeout_sec=60,
)
# result.verdict == Verdict.CONFIRMED  (axiom-free, ~1200 ms)

Default allow_axioms = Mathlib base [propext, Classical.choice, Quot.sound]. sorry / native_decide / disallowed axioms are routed to HOLDING.

search_counterexample

from rei_verify.search import search_counterexample

result = search_counterexample(
    claim="no n in [1,100] equals 42",
    predicate=lambda x: x == 42,
    space=range(1, 101),
    audit=audit,
    space_description="range(1, 101)",
)
# result.verdict == Verdict.REFUTED  (witness marker: n=42)

• exhaustion → HOLDING (search_space marker, 'absence ≠ proof')

• time/sample budget → HOLDING (compute_budget marker)

assert_breakpoints

from rei_verify.breakpoint import Breakpoint, assert_breakpoints

result = assert_breakpoints(
    claim="Collatz t1=1 orbits descend",
    breakpoints=[
        Breakpoint("n=27", assertion=lambda: descent(27), context={"n": 27}),
        Breakpoint("n=703", assertion=lambda: descent(703), context={"n": 703}),
        Breakpoint("n=6171", assertion=lambda: descent(6171), context={"n": 6171}),
    ],
    audit=audit,
    stop_on_first_failure=True,  # False で 全 breakpoint 実行 (集計目的)
)

• Any breakpoint False → REFUTED (label + context as witness)

• All pass → HOLDING ('listed checkpoints exhausted ≠ full case coverage')

hold_verdict

from rei_verify.hold import hold_verdict

result = hold_verdict(
    claim="my analytical claim under investigation",
    markers=[
        IncompleteMarker(
            dimension="search_space",
            what_was_tried="5 counterexample approaches",
            what_was_not_tried="structural refutation via categorical semantics",
            reason="categorical angle deferred to next session",
        ),
    ],
    audit=audit,
    notes="manual reasoning pause",
    require_multi_dimension=True,  # 単一 dim なら augmentation marker 追加
)
# result.verdict == Verdict.HOLDING  (audit chain 4 phase entries + caller markers)

Usage — MCP (Claude Desktop)

claude_desktop_config.json:

{
  "mcpServers": {
    "rei-verify": {
      "command": "python",
      "args": ["-m", "rei_verify"]
    }
  }
}

or (installed script):

{
  "mcpServers": {
    "rei-verify": {
      "command": "rei-verify"
    }
  }
}

MCP expression examples (x bind for search, ctx bind for breakpoints):

{
  "tool": "search_counterexample_explicit",
  "arguments": {
    "chain_id": "chain-abc123",
    "claim": "no perfect square in [1,100] equals 42",
    "samples": [1, 4, 9, 16, 25, 36, 49, 64, 81, 100],
    "predicate_expr": "x == 42",
    "space_description": "perfect squares up to 100"
  }
}

{
  "tool": "assert_breakpoints_explicit",
  "arguments": {
    "chain_id": "chain-abc123",
    "claim": "Collatz t1=1 descent",
    "breakpoints": [
      {"label": "n=27 case", "assertion_expr": "ctx['descent'] < 0",
       "context": {"n": 27, "descent": -0.5}},
      {"label": "n=703 case", "assertion_expr": "ctx['descent'] < 0",
       "context": {"n": 703, "descent": 0.2}}
    ]
  }
}

Integration demo

examples/collatz_t1_ones_lyapunov_demo.py — Executes a Lyapunov α-descent scan of Collatz odd n with trailing_ones(n)=1 using assert_breakpoints.

python examples/collatz_t1_ones_lyapunov_demo.py

Sample output (1,048,575 samples / 76.7 ms):

α=0.5〜0.85: WITNESS  n=9         r(n)=0.885622  → α refuted ✓
α=0.9:       WITNESS  n=17        r(n)=0.905315  → α refuted ✓
α=0.93:      WITNESS  n=57        r(n)=0.930288  → α refuted ✓
α=0.95:      WITNESS  n=313       r(n)=0.950121  → α refuted ✓
α=0.97:      WITNESS  n=14,601    r(n)=0.970001  → α refuted ✓
α=0.99:      NO WITNESS in range  max r=0.981135 < 0.99  → α NOT refuted in sample

VERDICT: REFUTED  (α=0.99 が サンプル範囲 で 未 refute = finite absence report)
audit chain: 6 entries、 sha256 hash chain intact

Witness n increases as α tightens (n=9 → n=14,601) = directly observing a finite reflection of r(n) → 1 as n → ∞, a practical example where the tool adheres to the discipline of "not automatically promoting finite absence to CONFIRMED". See demo comments for detailed honest scope.

Test coverage

Total 198/0 PASS (6 test files):

# individual
python test/test_skeleton.py
python test/test_refute.py       # requires 'lean' on PATH for live smoke

# all
for f in test/test_*.py; do PYTHONIOENCODING=utf-8 python -u "$f" | tail -3; done

For maintainers: PyPI Trusted Publisher setup

This repo's .github/workflows/publish.yml performs PyPI production publish on v tag push* + TestPyPI dry-run on workflow_dispatch. Before use, Trusted Publisher registration on both PyPI and TestPyPI sides and GitHub Environment creation are required.

See TRUSTED_PUBLISHER_SETUP.md for detailed steps.

⚠️ Double-check workflow.yml and Trusted Publisher registration before pushing tags (to prevent "tag = release trigger" accidents).

Design

See DESIGN.md for full rationale (8 sections):

• Design starting point (4 principles of Rei stack)

• 4 primitives details

• Verdict rule table (single source of truth)

• Refutation machine 3+1 tool mapping

• Relationship with framing-drift-detector

• Non-goals (out of scope for skeleton)

• Dependencies (intent of zero external deps)

• Honest scope

Related

• fc0web/rei-automator-mcp — Windows PC automation MCP, origin of AuditChain (generic extraction from STEP 1340 AuditLogWriter)

• fc0web/grounded — Prose grounding checker (2-tier verification)

• fc0web/grounding-check — SCPI hardware grounding checker

Author

Nobuki Fujimoto

License

MIT (v0.x irrevocable). Possibility of AGPL-3.0 + commercial dual from v1.0+. See LICENSE.

Honest scope (non-negotiable boundaries)

• (i) The skeleton's refutation tools only directly interface with Lean 4 (single-file lean execution); Mathlib-dependent proofs are a separate iteration (via lake project)

• (ii) The IncompleteMarker.dimension vocabulary is initially only 4 types; expansion will come from operational experience

• (iii) Hash chain is for tamper detection; cryptographic signing (Sigstore, etc.) is a separate concern

• (iv) Restricted eval is weaker than AST-level analysis (asteval, etc.); high-trust requirements will add dependencies in a separate iteration

• (v) Zero novelty claims for the "refutation machine" ([[feedback-world-uniqueness-claim-controllable]]) = only an integrated discipline layer of property-based testing (Hypothesis) + Lean 4 sorry-check + Coq/Isabelle-style industry standards; novelty is only the combinatorial discipline of "type-level integration of 4-value verdict + marker invariant + hash chain + MCP wrapper"

• (vi) The integration demo (Collatz t1=1) is not a reproduction of Fujimoto-san's actual Lyapunov analysis — only a simplified V = log2(n) and demonstration of TOOL behavior on a finite sample; true reproduction via Fujimoto-san's actual V + conditions + Lean 4 formalization is a separate iteration

• (vii) The "sorry-free" determination of refute_lean depends on #print axioms = if there is a kernel bug in Lean itself, it will not be verified (kernel bug is outside Rei scope)