ResiMind

ResiMind — Verified Memory for AI Agents

Catch the error. Keep the insight. Give the next task a checked head start.

Run the demo · Connect MCP · Install the Skill · Take the challenge · 中文

Frontier roadmap and evidence · External theorem benchmark boundary

Latest on `main` (after v0.16.0): memory provenance, expiry and transfer auditing, reserved revision steps in the ChinaTravel integration, and an experimental external Lean template compiler. The latest same-model planning result and development rerun are published with their failures; neither establishes a planning success-rate gain. MiniF2F and LeanDojo scores are still pending.

ResiMind is an open-source neuro-symbolic Agent architecture that connects independent verification, residual-guided self-correction and reusable rule memory. Your model, rules or symbolic tools propose a step; domain checks decide what becomes a fact. Failed checks tell the next attempt what still needs fixing.

A checked solution can become a checked rule. Explicit learning extracts candidate rules from completed derivations, independently verifies admission, and rechecks each future application. Knowledge grows outside the model, without changing its weights. When local rules or tools suffice, the supported math routes run with zero model calls.

Formal memory can now compose checked conditions. The bounded Lean planner introduces an implication, applies a verified conditional lemma, and sends the resulting residual subgoal to another verified lemma or a local assumption. The whole typed plan is compiled again by Lean; structural matching never counts as proof. This is an experimental composition primitive, not a claim of MiniF2F or general theorem-proving leadership.

The core also runs bridge engineering, constrained optimization, customer support and open-ended planning with their own verifiers. Adaptive algebra, rule learning and the five MCP tools currently cover bounded rational polynomials. Core: Python 3.10+, no runtime dependencies. Optional MCP: Python 3.11+.

Created and originally published by @1105216375-alt. Citation · Changelog

Evaluating tools for your Agent? Make this one catch a wrong answer first. Run the nine-call integration probe: reject → repair → learn → recall, including an unsupported-scope control. No model key. Machine-readable cases · Documentation index

Try it in three minutes

With Python installed:

git clone https://github.com/1105216375-alt/resimind.git

cd resimind python -m venv .venv source .venv/bin/activate python -m pip install . python -m resimind demo --domain lifelong

On Windows PowerShell, activate with .venv\Scripts\Activate.ps1. Installation may download build tools. The demo runs offline, without an API key; both python -m resimind and the installed resimind command work outside the checkout.

The first demo solves two training problems, extracts a checked rule, saves and reloads frozen memory, and transfers that rule to new coefficients. It then solves a long expansion using a sparse certificate. The frozen memory stays unchanged throughout evaluation. No API calls are made.

All demo commands: math, bridges, planning, support and Lean

Choose a different challenge. These commands run offline; the Lean example additionally requires an installed Lean 4.29.0 toolchain:

Add --json to inspect the audit. Connect DeepSeek when you want the model to compose its own plan.

Watch it recover. Then watch it reuse what worked.

The adaptive demo deliberately proposes a wrong expansion, rejects it, changes approach, completes a proof, and reuses its checked rule on a new-variable task. Its proposals are scripted; the verification, state transitions, admission and reuse really execute.

See a rule cross the task boundary

Run these in one process after installing the core (Bash/Zsh; see the JSON-lines guide for the request format):

python -m resimind api <<'JSONL'

{"tool":"verify_identity","arguments":{"lhs":"(x+1)2","rhs":"x2+1","variables":["x"]}} {"tool":"learn_polynomial","arguments":{"expression":"(a+b)3","variables":["a","b"]}} {"tool":"learn_polynomial","arguments":{"expression":"(u+v)3","variables":["u","v"]}} {"tool":"recall_polynomial","arguments":{"expression":"(2*x+3*y)**3","variables":["x","y"]}} JSONL

What to look for: the false identity is rejected; the first learning example adds no rule; the second compatible example produces an independently checked cubic schema. Recall uses it on new coefficients in one rule action, zero model calls, followed by exact verification. This is a reproducible example, not a general performance claim. Response fields, bounds and persistent Python memory →

Can your Agent catch the wrong step?

Give it 28 public polynomial tasks: 12 correct chains, 12 mutated chains and 4 unsupported controls. Ask it to locate the first wrong step, repair it, and respect the supported scope. An independent SymPy scorer checks the submissions.

Try the challenge → · Install the verify-and-repair Skill → · Searchable task examples →

Pick a problem you can inspect

| Customer support | A refund