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 · 中文

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.

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":"x**2+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

Open-ended planning: many answers, explicit constraints

The request: “Plan a relaxed day with art and a meal. I like quiet places and coffee.”

The supplied hard constraints are 09:00–18:00, ¥300 for one person, at most 45 minutes walking, at least three distinct stops, art and a meal, and a return to the starting station. Opening windows, minimum visit durations, and every travel leg must also fit. Quietness and coffee begin as preferences; the later experiment makes coffee mandatory.

Same request, different valid answers

The model can choose places, order, timing, and transport. The verifier accepts a whole plan that satisfies the constraints, without comparing it to one fixed answer. These two independently checked offline examples satisfy the same original request:

Venue and transport data are fictional. These checks establish feasibility under the supplied inputs; enjoyment and the “best day” remain subjective. Inspect the schedules and transport choices.

A constraint fails: inspect the feedback and revision

These are executable offline fixtures, with deliberately flawed candidates. The checks and state transitions really execute; these mistakes are not attributed to a live model.

The neuro-symbolic interaction: neural proposals explore the choices, symbolic checks enforce the explicit constraints, and residual feedback tells the next proposal what still needs fixing or evidence.

Change the requirement. Watch the plan change.

A real DeepSeek run proposed gallery → noodles → reading room. It satisfied the original constraints. We then made coffee mandatory in the structured requirements and resubmitted that actual plan:

The model chooses among possible plans; the verifier enforces the requirements. The cafe covers both a meal and coffee in the fictional catalog. This recorded experiment uses synthetic venue and transport data; the check establishes feasibility under those inputs.

Inspect both proposals, the rejection, and the checked revision →

Full planning rules and all three offline scenarios · Runnable example · Real DeepSeek audits

Use the standalone Agent

ResiMind owns the reasoning loop: collect evidence, propose, verify, commit facts, and rebuild remaining obligations. Run it directly:

from resimind import Task
from resimind.domains.planning import DOMAIN, build_agent, demo_problem, verified_plan

agent = build_agent(demo_problem())  # Offline; inject complete=your_model for neural proposals.
result = agent.run(Task("day-out", "Plan a relaxed day with art and a meal.", DOMAIN))
run = result.run_result
if run.status == "solved" and run.residual.solved:
    print(verified_plan(result))
else:
    print("Still unresolved:", run.residual.pending)

Model SDKs and external workflow connectors are optional integrations. No LangGraph installation is needed for this Agent or the built-in domain demos.

Customer support: check a refund before promising one

A customer asks to return an order. The recorded item payment is ¥249, with ¥10 shipping. Under the example merchant's configured policy, shipping is excluded from this quote.

python -m resimind demo --domain customer-support
python -m resimind demo --domain customer-support --scenario missing-delivery
python -m resimind demo --domain customer-support --scenario expired

These are offline demonstrations using fictional merchant rules and synthetic orders. The Agent prepares a recommendation; it does not execute a refund or claim that money has arrived. A missing-evidence run exits nonzero because the task is still open. You can also connect a real DeepSeek callback.

Read the customer-support adapter and live example → · Actual DeepSeek run: 5 calls, 2 rejected proposals, verified recommendation

Mathematics: a solution is not yet a proof

Learn a reusable step from a completed proof: the new knowledge-growth Agent adds a second loop: verified derivation → candidate rule → independent admission → persistent library → future proposals. Its polynomial demo uses a deterministic rewrite grammar; a model callback can supply proposals through the same gate. Recorded results measure offline rule reuse, not neural mathematical discovery.

Static trace. This is an executed offline fixture with a deliberately infeasible candidate.

Minimize a three-variable quadratic with coupled terms, an equality constraint, nonnegativity, and an upper bound:

$$ \min_x;2x_1^2+x_1x_2+x_2^2+x_3^2-8x_1-3x_2-3x_3, \quad x_1+x_2+x_3=3,\quad x\geq0,\quad x_1\leq1. $$

The initial equality-stationary proposal is (26/15, 1/5, 16/15). Its objective is lower, but it violates x1 <= 1: the verifier rejects it. After feedback, the Agent proposes (1, 3/4, 5/4) with objective −73/8.

That answer alone cannot close the task. The verifier must check exact LDLᵀ positive-definiteness, primal feasibility, KKT stationarity and complementarity, and a polynomial global-optimality certificate. All arithmetic uses rational numbers. The offline proposer searches active sets; the verifier checks the submitted certificate without running that search.

python -m examples.constrained_optimization
python -m examples.constrained_optimization --json

ACCEPT certify_convexity   → positive_definiteness_verified   (2 remaining)
REJECT certify_primal_dual → primal_inequality_violation      (2 remaining)
ACCEPT certify_primal_dual → primal_and_kkt_verified          (1 remaining)
ACCEPT certify_global     → global_gap_identity_verified     (0 remaining)

Read the problem, proof, and failure cases →

Bridge engineering: continuity changes the answer

Analyze a synthetic 24 m + 30 m two-span continuous bridge girder with unequal flexural stiffness, dead load, left/right/both-span live loading, and two supplied load combinations: eight cases in total.

The first proposal treats the spans as independent simply supported beams. It can balance forces and still be wrong: the rotations at the shared pier must agree. The verifier checks the beam equations and displacement compatibility before accepting the corrected continuous-beam solution.

The Agent then has to account for every required load case, calculate support reactions and positive/negative moment extrema, form the case envelope, and compare supplied moment and midspan-deflection limits. Omitting a pattern leaves outstanding obligations; a checked limit exceedance remains a valid completed analysis.

python -m examples.continuous_bridge
python -m examples.continuous_bridge --json

Read the structural model, equations, and limits →

Both showcases execute real checks with deterministic offline proposers and deliberately invalid candidates. Supply a model callback to use neural proposals. These runs demonstrate verification behavior, not LLM accuracy. The bridge is a synthetic equivalent line-beam example with supplied limits, not a design-code assessment; its midpoint checks are not a global deflection envelope.

Included domain adapters

solved means the declared obligations are complete. It does not automatically mean a feasible solution exists or an engineering limit is satisfied. Each adapter has a bounded scope; the shared core makes those checks explicit.

Where the neuro-symbolic part lives

Neural proposals. ModelProposer accepts a provider-neutral complete(prompt: str) -> str callback. A real model can choose a registered action and propose a claim with evidence references. The domain builders accept build_agent(problem, complete=your_complete). The callback receives current state, outstanding obligations, evidence, allowed actions, and the last verifier feedback; it returns a JSON candidate or null.

Symbolic checks. Trusted domain code independently recomputes results and checks references, prerequisites, scope, exact rational arithmetic, and units. The verifier creates the facts that may be committed. A model cannot grant itself verification with a confidence score or a verified field.

Residual feedback. A residual is the set of outstanding goals, unknowns, and hard constraints. It is rebuilt from committed facts. A rejection preserves state and returns its reason to the proposer; a missing prerequisite keeps the task open.

Knowledge growth. LearningAgent extracts candidate knowledge from completed derivations. KnowledgeLibrary delegates admission to the registered domain verifier, supports save/reload with re-verification and revocation, and retrieves rules as proposal guidance. Current-task verification still applies.

Formal residual composition. resimind.integrations.formal.solve can search a bounded chain of implication lemmas and local assumptions. It records the residual plan, then recompiles the complete intro/apply/exact tree through Lean. The planner is a new composition primitive; the repository does not claim an external theorem-proving leaderboard result until a frozen miniF2F/LeanDojo evaluation exists.

Reusable architecture extensions. ObligationGraph tracks dependency-aware residual work and evidence invalidation; StrategyPolicy ranks already registered strategies from frozen observations; and the structural rule extractor proposes narrow schemas only after exact verification. These helpers never authorize facts or replace the domain verifier.

Models connect through callbacks; the project develops Agent reasoning, verification, and knowledge admission. The algebra proof checker has explicit expression and resource limits. See knowledge growth and the neuro-symbolic implementation map.

The architecture

flowchart LR
    T[Task] --> A[Agent]
    A --> E[Evidence tools]
    A --> P[Model / rule proposer]
    E --> P
    M[Reviewed route memory] --> P
    R[Residual obligations] --> P
    P --> C[Candidate + references]
    C --> V[Independent verifier]
    E --> V
    V -->|accept + binding checks| F[Commit verified facts]
    V -->|reject / defer + feedback| P
    V -->|interrupt| H[Stop and hand off]
    F --> D[Rebuild residual]
    D --> R
    F --> O[Facts + JSON audit trail]
    D -->|task complete| X[Extract derivation certificate]
    X --> K[Independent knowledge admission]
    K -->|verified| L[Persistent knowledge library]
    L -->|retrieve; application rechecked| P

• Evidence before claims: registered tools collect typed inputs for each task.
• Verification before state changes: verdicts bind to candidate, state, and evidence; commits check references and conflicts atomically.
• Explicit unfinished work: goals, unknowns, and hard constraints remain visible until discharged by the domain adapter.
• Knowledge that carries forward: completed derivations face independent admission, re-verification on reload, and checks on every new application.
• Reusable routes: in-memory routes require review and matching applicability; reused steps still need verification on current inputs.
• Inspectable execution: every attempt records its decision, reason, state, and residual; attempt and stall budgets bound the loop.

Build your own adapter

Implement three small interfaces:

Assemble them with Agent, Task, registered EvidenceTool objects, and optional RouteMemory. The core does not import either reference domain. See the adapter guide and domain contract for connecting your own calculation, simulation, rule checker, or proof tool. These detailed guides are currently in Chinese; neuro-symbolic.md provides an English implementation map.

Optional integrations

The standalone ResiMind Agent remains responsible for proposal, verification, and residual feedback. Add only the integration your application needs:

For live planning, run from a checkout:

python -m pip install '.[deepseek]'
# Set DEEPSEEK_API_KEY and DEEPSEEK_MODEL in your local environment first.
python -m examples.open_planning --live --json

Live calls can incur provider charges and can remain unresolved. The model guide documents request budgets and timeouts; there is no offline fallback after a failed live request. Validation distinguishes actual live records from simulated transport tests.

LangGraph is an optional outer connector. The ResiMind core and all domain adapters run without it. Use its verification subgraph when integrating with an existing LangGraph project; it forwards checked facts or unresolved obligations and does not supply additional domain verification rules.

More examples and checks

python -m examples.agent_demo       # task → tool → model callback → verifier
python -m examples.inventory        # independent recomputation and rejection
python -m examples.document_review  # missing evidence stays unresolved
python -m examples.route_memory     # review, applicability, and revocation
python -m pip install -e '.[dev]'
python -m pytest -q

See v0.16.0 release validation for current checks, and the v0.14.0 record, v0.13.0 record, v0.12.1 record, v0.12.0 record, v0.11.0 record, v0.10.0 record, v0.9.0 record, v0.8.0 record, knowledge-growth development record and earlier version record for historical checks.

Derive once. Reuse on a new task.

An Agent derives the square and cube identities, submits their proof chains for independent admission, saves its library, and reloads it with verification. New tasks can retrieve those rules; each application must still pass the current task's checks.

71.4% fewer transfer proposals, with 13 additional proposals to learn the rules. Both arms use the same deterministic proposer and budget. This measures reuse on published development tasks; it does not measure a model accuracy gain or total compute savings.

How rules are proved, admitted, stored, revoked, and reused → · Reproduce the comparison · Validation

Measure the Agent, not the model

Keep the model, tasks, and resource ceilings fixed; measure completion, invalid deliveries, calls, and cross-task reuse. These studies use different tasks and budgets, so their results are reported separately:

Related systems (中文) compares the project with orchestration frameworks, verifier-driven reasoning, and knowledge-accumulating agents.

Current scope

ResiMind is an experimental, synchronous Agent framework. Tool evidence is collected before the loop. It includes optional DeepSeek/OpenAI callbacks, a LangGraph verification subgraph, bounded search, and an independently checked knowledge library with JSON persistence. The bounded algebra adapter implements the derivation-to-reuse learning loop. Dynamic tool scheduling, automatic multi-role planning, general CAS/SMT/prover connectors, and distributed execution are not included.

Domain verifiers and residual builders are trusted application code; their correctness determines what solved means. Evidence labels do not authenticate real-world inputs. Digests catch result mix-ups, not malicious plugins. Callers must enforce model/tool timeouts and resource limits; step budgets cannot interrupt a blocked callback. The optional model wrappers bound response tokens and API attempts; these are not a total-cost cap or a hard deadline for the full run.

This repository contains a generic implementation and synthetic examples distilled from the Bridge Doctor application's workflow. It contains no original application records, customer data, credentials, or private model logs. Read provenance, architecture and trust boundaries, and security.

Authorship and citation

ResiMind was initiated and originally published by @1105216375-alt, drawing on the creator's Bridge Doctor application. The original repository is 1105216375-alt/resimind; its releases record published versions. See provenance for the extraction scope.

If you use or discuss ResiMind, please cite the project and link to the original repository. Suggested citation:

1105216375-alt. ResiMind (version 0.16.0), 2026. https://github.com/1105216375-alt/resimind

Machine-readable citation metadata is provided in CITATION.cff. Citation is appreciated, not an additional license condition. Commercial use is permitted under the MIT License, which requires retaining its copyright and permission notices in copies or substantial portions of the software.

New domain adapters, counterexamples, and verifier failure tests are welcome. See CONTRIBUTING.md.