lean4-memories
PassAudited by ClawScan on May 10, 2026.
Overview
This Lean 4 memory skill is purpose-aligned, but it stores proof context and preferences in persistent MCP memory, so users should understand and trust the memory backend.
This skill appears benign and aligned with Lean 4 proof assistance. Before installing, make sure you trust the MCP memory server being used, avoid saving secrets or private unrelated content, and review stored memories periodically because they can influence future proof sessions.
Findings (3)
Artifact-based informational review of SKILL.md, metadata, install specs, static scan signals, and capability signals. ClawScan does not execute the skill or run runtime probes.
Future Lean proof suggestions may be shaped by stored memories, including old failed approaches, project conventions, and preferences.
The skill intentionally stores reusable context across sessions. This is purpose-aligned, but persistent memories can contain project details or user preferences and may influence future agent behavior if stale or inaccurate.
maintain persistent memory of successful proof patterns, failed approaches, project conventions, and user preferences across sessions
Use project-scoped memory, avoid storing secrets or private non-proof content, and periodically review or remove stale memories.
Project metadata, proof patterns, filenames, and preferences may be stored wherever the configured MCP memory server keeps its data.
The skill depends on an MCP memory server for storage/retrieval. That is expected for the skill, but the artifacts do not define the server’s storage location, sharing model, or trust boundary.
This script assumes MCP memory server is configured and available.
Connect only to a trusted MCP memory server, understand whether it is local or shared, and confirm what data it stores or syncs.
The visible helper script does not appear dangerous, but actual memory-server behavior depends on the user’s configured MCP components.
The helper script is presented as a template/simulation and does not implement actual MCP calls in the provided code. Users relying on a real MCP implementation should verify any additional server or client code not shown here.
For now, this is a template showing the structure and interface
Review the MCP memory server/client configuration separately before using it for project or team memory.