rei-verify

Máquina de refutación — especializada en negación, no en generación. Infraestructura de verificación + servidor MCP.

Versión: 0.1.0a1 (2026-08-19) — 4 primitivas + 4 herramientas de refutación + 8 herramientas MCP + demo de integración. Test 198/0 PASS.

Por qué «máquina de refutación»

La generación se satura. La refutación no se satura.

Los LLM actuales son fluidos. Pueden generar líneas de razonamiento plausibles, código plausible, nombres de teoremas plausibles, independientemente de si son ciertos. Aunque los benchmarks se saturen al 96%, esta estructura no cambia. Lo que falta en el mundo no es una «máquina para crear cosas plausibles», sino una «máquina para matar cosas plausibles de forma fiable».

La promesa central de la máquina de refutación:

• Al recibir una afirmación, dedica recursos computacionales a buscar contraejemplos. Los intentos de demostración quedan en segundo plano.

• Si no se encuentra un contraejemplo, devuelve explícitamente «la forma del espacio de búsqueda donde no se encontró» (no disfraza el silencio como éxito).

• La salida siempre incluye «el lugar donde la afirmación se rompería si fuera falsa». Lean 4 con cero sorry es el caso especial más estricto de esto.

• «No se pudo refutar» y «es correcto» se tratan como cosas diferentes a nivel de tipos.

Related MCP server: prova-mcp

Veredicto de 4 valores («disciplina central de no mentir jamás»)

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 でない

No usar TRUE/FALSE binario = no refutado ≠ correcto. Tipificación de la disciplina de 12 años de IUT holding.

Garantía de tipo «no disfrazar el silencio como éxito»: todos los veredictos excepto CONFIRMED deben incluir al menos 1 IncompleteMarker (dimensión + qué_se_intentó + qué_no_se_intentó + razón) (invariante de dataclass, irrompible).

4 primitivas (rei_verify)

4 herramientas de refutación (rei_verify.*)

El corazón de la máquina de refutación. Todas las herramientas devuelven VerdictWithMarkers (veredicto de 4 valores + marcadores + audit_hashes) con una forma consistente.

★ La única herramienta que emite CONFIRMED es refute_lean_source (solo en casos donde el kernel de Lean 4 certifica que no hay sorry). Las otras 3 herramientas siempre devuelven REFUTED o HOLDING = garantía a nivel de tipo de la disciplina «ausencia de contraejemplo no es prueba».

8 herramientas MCP

Se pueden llamar directamente desde clientes LLM como Claude Desktop / Cursor / Cline:

Las expresiones seguras para MCP usan eval restringido = se rechazan previamente __import__ / exec / eval / open / prefijo __, solo se permite la lista blanca _SAFE_BUILTINS (abs/min/max/sum/len/int/float/str/bool/round/any/all/range).

Instalación

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

o desde el código fuente:

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

Requiere Python 3.10+ (dataclass + Enum + nuevas funciones de tipado). Las primitivas principales funcionan solo con la biblioteca estándar (se pueden importar aunque el paquete mcp no esté presente).

Uso — como biblioteca

VerifiedExecution (personalizado)

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)

Axiomas permitidos por defecto = base de Mathlib [propext, Classical.choice, Quot.sound]. sorry / native_decide / axioma no permitido se enrutan a 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)

• agotamiento → HOLDING (marcador search_space, «ausencia ≠ prueba»)

• límite de tiempo/muestras → HOLDING (marcador compute_budget)

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 実行 (集計目的)
)

• Cualquier breakpoint False → REFUTED (etiqueta + contexto como testigo)

• Todos pasan → HOLDING («puntos de control listados agotados ≠ todos los casos cubiertos»)

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)

Uso — MCP (Claude Desktop)

claude_desktop_config.json:

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

o (script instalado):

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

Ejemplo de expresión MCP (x bind para búsqueda, ctx bind para 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}}
    ]
  }
}

Demo de integración

examples/collatz_t1_ones_lyapunov_demo.py — Escaneo de descenso α de Lyapunov para números impares de Collatz con trailing_ones(n)=1 usando assert_breakpoints.

python examples/collatz_t1_ones_lyapunov_demo.py

Salida de ejemplo (1.048.575 muestras / 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

El testigo n aumenta a medida que α se ajusta (n=9 → n=14.601) = observación directa de la reflexión finita de r(n) → 1 cuando n → ∞, ejemplo real de que la herramienta cumple la disciplina de «no promocionar automáticamente ausencia finita a CONFIRMED». Consulte los comentarios en la demo para un alcance honesto detallado.

Cobertura de pruebas

Acumulado 198/0 PASS (6 archivos de prueba):

# 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

Para mantenedores: configuración de PyPI Trusted Publisher

El archivo .github/workflows/publish.yml de este repositorio realiza publicación en PyPI producción con push de etiqueta v* + dry-run en TestPyPI con workflow_dispatch. Antes de usarlo, se requiere el registro de Trusted Publisher tanto en PyPI como en TestPyPI, y la creación del entorno de GitHub.

Consulte TRUSTED_PUBLISHER_SETUP.md para instrucciones detalladas.

⚠️ Antes de hacer push de una etiqueta, verifique doblemente workflow.yml + registro de Trusted Publisher (para evitar accidentes de «etiqueta = disparador de lanzamiento»).

Diseño

Consulte DESIGN.md para la justificación completa (8 secciones):

• Punto de partida del diseño (4 principios de la pila Rei)

• Detalles de las 4 primitivas

• Tabla de reglas de veredicto (fuente única de verdad)

• Mapeo de herramientas 3+1 de la máquina de refutación

• Relación con el detector de desviación de marco

• No objetivos (fuera del alcance del esqueleto)

• Dependencias (intención de cero dependencias externas)

• Alcance honesto

Relacionado

• fc0web/rei-automator-mcp — Automatización MCP para PC Windows, origen de AuditChain (extracción genérica de STEP 1340 AuditLogWriter)

• fc0web/grounded — Comprobador de fundamentación en prosa (verificación de 2 niveles)

• fc0web/grounding-check — Comprobador de conexión a tierra de hardware SCPI

Autor

Nobuki Fujimoto

Licencia

MIT (v0.x irrevocable). Posible AGPL-3.0 + dual comercial a partir de v1.0+. Consulte LICENSE.

Alcance honesto (líneas no negociables)

• (i) Las herramientas de refutación del esqueleto solo interactúan directamente con Lean 4 (ejecución de un solo archivo lean); las pruebas que dependen de Mathlib son una iteración aparte (a través de un proyecto lake)

• (ii) El vocabulario IncompleteMarker.dimension es solo de 4 tipos inicialmente; la ampliación se basará en la experiencia operativa

• (iii) La cadena hash es para detección de manipulación; la firma criptográfica (Sigstore, etc.) es una preocupación aparte

• (iv) El eval restringido es más débil que el análisis a nivel de AST (asteval, etc.); los requisitos de alta confianza requerirán añadir dependencias en otra iteración

• (v) Reclamación de novedad cero para la «máquina de refutación» ([[feedback-world-uniqueness-claim-controllable]]) = solo una capa de disciplina de integración de pruebas basadas en propiedades (Hypothesis) + comprobación de sorry en Lean 4 + estándares de la industria de Coq / Isabelle; la novedad es solo la combinación disciplinaria de «veredicto de 4 valores + invariante de marcador + cadena hash + envoltorio MCP»

• (vi) La demo de integración (Collatz t1=1) no es una reproducción del análisis real de Lyapunov de Fujimoto — es solo una simplificación con V = log2(n) y muestras finitas para demostrar el funcionamiento de la HERRAMIENTA; la verdadera reproducción requiere la V real de Fujimoto + condiciones + formalización en Lean 4, en otra iteración

• (vii) La determinación de «sin sorry» de refute_lean depende de #print axioms = si el propio kernel de Lean tiene un error, no se verificará (los errores del kernel están fuera del alcance de Rei)