1105216375-alt / 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+.
| What you want to do | Your entry point |
| --- | --- |
| Give an existing Agent exact algebra tools | MCP setup · Download MCPB |
| Teach an Agent a bounded verify-and-repair workflow | Repair Skill · Install guide |
| Build an Agent with your own checks | Architecture · Adapter contract |
| Inspect what has actually been measured | Evidence · Release validation |
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:
 [code] 
On Windows PowerShell, activate with `.venv\Scripts\Activate.ps1`. Installation may download build tools. The demo runs **offline, without an API key**; both