memcp: token-efficient, multi-project, multi-surface external memory for AI agents written in SPARK Silver

This post describes work on a personal/hobby project undertaken by a member of AdaCore’s technical staff. We’re publishing it here because we think the topic and the takeaways will be of interest and value to the Ada community.

If you’ve spent time using AI agents, you may have found yourself frustrated that a lesson or decision from a prior session isn’t available in your current session. Some agents have an internal memory system that attempts to solve the problem, but it tends to be hit-or-miss, project-specific, and surface-specific: if you move to a new project or move your same project to another surface, the memory is unavailable.

When mempalace went viral, I became excited by the possibility of solving this problem. So I forked mempalace, extended it to work across multiple isolated environments (multi-surface) using a Python MCP-server library (FastMCP) so all of my sessions could connect back to a central data store using MCP over HTTP (with SSH port-forwarding handling authentication and transport security), and was generally happy for a while. But I discovered that the central conceit of mempalace - the “mind-palace”-inspired organization - brought no benefit and, more importantly, it was extremely token inefficient, not having been designed for progressive disclosure.

So I rolled my own memory system, based on my experience and knowing precisely what I wanted. I created a first implementation of memcp - a token-efficient, multi-project, multi-surface external memory - in Python using FastMCP, sentence-transformers, and sqlite-vec. I’ve used it for months and have been very happy with it.

memcp works and works well. So I wondered: how hard would it be to rewrite it in SPARK and prove it to Silver (absence of runtime errors, including proven memory safety)?

The answer: not hard at all. I led the translation from the Python reference implementation to SPARK; my agent wrote 100% of the code; I reviewed, providing feedback, judgment, and SPARK expertise where needed. All in all, in just over a week from start to finish of largely background effort (not eight-hour days!), I had not just a working system, but a really nice SPARK implementation of memcp proved to Silver. No pragma Assumes, no checks justified as false positives. AI agents running frontier models are now able to write ordinary SPARK unaided and prove that code to Silver unaided. The residual human attention and expertise is now concentrated at the boundaries, where SPARK’s model of the world must be supplied by hand. We’ll dig into the examples I encountered below.

You can find the repository here. I encourage you to clone it, use it, fork it, and contribute to it. I think it’s great; I hope you will too!

What is memcp?

memcp is an external memory for your AI agent.

At startup, a hook injects five 100-character “headlines” from the five most recent sessions in the given project across all surfaces into the agent’s context. From there, based on the user’s first and subsequent turns, the agent can decide if information from any of those sessions would be relevant and retrieve first an agent-authored summary of a given session before drilling down further by retrieving verbatim user/agent turns from that session as needed. At the end of a session, the user instructs the agent to “save a summary for memcp” and it does so, generating the headline and summary for future retrieval. When the user closes the session, regardless of whether or not they’ve generated a summary, the complete session is sent to the memcp server, mined for agent/user turns (excluding tool calls and results), and stored verbatim. (The complete session contents including tool calls and results are never made available to the agent through memcp; they’re stored for posterity.) If the user forgets or chooses not to save a summary, a headline is generated from the agent’s “recap” if available and, no matter what, the verbatim turns are available to the agent during search.

The system is token-efficient because of the progressive disclosure from heading to summary to raw turn chunks. The system is multi-project because, while the agent generally specifies the project to search, the default is to search across projects. The system is multi-surface because the MCP over HTTP allows all instances across all environments to read and write to a centralized data store.

memcp lets me do things like fire up my AI agent and ask “where are we and what’s next?” and expect a grounded answer. I can say “yesterday in project X we did Y; I want to apply that same approach to this project” and my agent can retrieve the details and start working. Or I can say “you wrote a handoff in the last turn of the last session; grab it and start working”. I’ll warn you, once you start using your agent this way, you won’t want to go back.

What parts of memcp are in SPARK?

It’s actually easier to answer this question by saying what’s not in SPARK. memcp uses three external libraries:

• tiny_http, a minimal HTTP server written in Rust
• candle, a torch replacement, written in Rust, and
• sqlite plus sqlite-vec, a C extension to sqlite that adds a vector store.

memcp binds to all three libraries using C foreign-function interfacing (FFI). The bindings are thick and therefore idiomatic: a small set of C FFI calls with SPARK Silver wrappers that expose an idiomatic SPARK interface to the rest of the program.

FFI is mechanically easy to do in SPARK, but tricky to get right because, perforce, SPARK cannot analyze what’s happening on the other side of the FFI boundary and must trust the user to provide it with information required to maintain the soundness of the analysis. I discuss this in more detail below.

Aside from the FFI calls to these three libraries, almost everything else is in SPARK, including JSON handling, and proved to SPARK Silver.

What was easy?

As I said above, I used AI to produce the SPARK implementation of memcp from the Python reference implementation. (No, this project was not vibe-coded: significant engineering and SPARK expertise went into it.) This initial pass, including rewriting json-ada into the SPARK Silver json-spark¹, was automatic, fast, and successful: all the code was produced, it worked (as much as can be expected for a first translation pass), and proved to SPARK Silver.

The initial pass also wasn’t complete. AI agents have gotten very good at writing SPARK and proving it to Silver - provided they’re working on “normal” SPARK code. And as time passes, more SPARK code appears to be “normal” to the agents. The progress since earlier this year is frankly breathtaking.

AI agents still struggle with SPARK at the “edges”. That was certainly the case here and where most of my effort and attention was spent.

All of the code related to handling of strings, JSON, setup, tool definition, tool calling, etc. was written and proved on the first pass. There were opportunities for minor improvements (name cleanup, documentation, more idiomatic Ada) that I and my collaborators took and are continuing to take. But this is expected, and the initial results were solid.

This is exciting! Compared to languages like Python, C or even Rust, SPARK is a low-resource language: there is vastly less SPARK in the datasets used to train models. Yet the frontier models and their agents have demonstrated incredible gains over the past six months. You can now choose to implement your next project in SPARK with confidence that your AI agent will be able to handle the bulk of the work, freeing you to focus on the requirements, design, and those parts of the code that might qualify as “edges”.

What was hard?

Essentially, everything that was hard on this project boiled down to the implications of FFI. To unpack that, there were really two major things that required my careful attention:

1. external abstract global state; and
2. ownership and reclamation of private types.

A contract is the only channel that carries information across a subprogram boundary in SPARK. This is fundamental to how assume-guarantee reasoning works in deductive formal verification. And while the frontier models should “understand” this concept (to the extent that a pile of statistics can be said to “understand” anything), they don’t - at least not to the extent that they are able to apply the concept in practice.

In SPARK, when subprogram Foo calls subprogram Bar:

• Foo
  • proves that Bar’s precondition holds at the point at which Foo calls Bar
  • assumes that Bar’s postcondition holds after Bar returns
• Bar
  • assumes that Bar’s precondition holds
  • proves that Bar’s postcondition holds

This allows SPARK to perform modular proof. When proving Bar, its uses are not considered. When proving Foo, the details of Bar are not considered. This assume-guarantee reasoning is essential to SPARK’s ability to prove programs of realistic size. But for an imported subprogram, a subprogram whose body is in a library and was possibly written in another language, that second half never happens: there is no body available for SPARK to analyze, so it cannot discharge the contract and must simply believe it.

External abstract global state

Frontier models have no difficulty in writing the Ada side of a binding, like this:

  procedure Close (Db : System.Address)
    with Import, Convention => C, External_Name => "sqlite3_close_v2";

This tells the compiler that it shouldn’t expect to find a body anywhere in the SPARK code, that the calling convention is C’s, and the name the linker should use to resolve this symbol at link time is sqlite3_close_v2, the name declared by the sqlite API.

What the AI agent did not know how to do was to declare to SPARK that Close reads and writes global state on the other side of the FFI boundary.

What happens if we don’t tell SPARK about this mutated global state? When we call Close, SPARK will tell us that we’ve made a call to a subprogram that has no effect. After all, Db, the sole formal parameter to Close, is an input (thus is not modified). And since SPARK cannot look on the other side of the FFI boundary and we’ve not said global state is modified, SPARK assumes no such modification.

Of course, Close does modify global state. In the sqlite engine, the resource referenced by Db is released (which is important, to avoid a resource leak). So we get an apparent nuisance warning on the call to Close because we’ve failed to be precise about how the FFI hides global state manipulation.

But it gets worse. We need to be able to poll the database for changes. The AI agent generated this piece of the binding like this:

  function Changes (Db : System.Address) return Interfaces.C.int
    with Import, Convention => C, External_Name => "sqlite3_changes";

Again, there’s no recognition here of global state nor that the global state is effectively volatile from SPARK’s point of view. And this leads us to potential unsoundness in our analysis.

SPARK requires that functions be pure, absent specific annotations to the contrary: like a mathematical function, if you call Foo multiple times with the same inputs, you get the same output. This extends to Changes: as written above, SPARK will assume that if you call Changes multiple times on the same Db, you’ll get the same answer.

This is, of course, not at all how Changes works. Why? Because there is global state on the other side of the FFI boundary that Changes reads. Moreover, that state is effectively volatile, so Changes is effectively volatile: multiple calls to Changes with the same actual parameter are not expected to return the same result.

SPARK’s warnings cannot be dismissed without careful review, when FFI is in play. They are often the only signal SPARK is able to give you that the model you’ve (implicitly, perhaps, by omission) claimed for the other side of the FFI boundary is incorrect and a potential source of unsoundness. Unfortunately, AI agents ignore these warnings by default. Initially, I had 148 (!) warnings that the agent was ignoring. When I was done, I had driven that to zero.

The solution to this class of problems is to declare abstract state, note that it is external, and to be precise (if needed) about which aspects of this state are volatile.

We declare the sqlite package like this:

package Sqlite_Vec_Spark
 with SPARK_Mode     => On,
      Abstract_State => (DBMS with External => (Async_Writers    => True,
                                                Async_Readers    => True,
                                                Effective_Writes => True,
                                                Effective_Reads  => False)),
      Initializes    => DBMS
is

Then, we are able to enhance the declarations of the FFI bindings like this:

  procedure Close (Db : System.Address)
    with Import, Convention => C, External_Name => "sqlite3_close_v2",
         Global => (In_Out => DBMS), Always_Terminates => True;

  function Changes (Db : System.Address) return Interfaces.C.int
    with Import, Convention => C, External_Name => "sqlite3_changes",
         Volatile_Function, Global => (Input => DBMS);

Now, SPARK knows:

• Close does modify global state; that’s the Global => (In_Out => DBMS). And because DBMS is declared Async_Readers => True and Effective_Writes => True, that write is effective: a peer may observe it, so flow analysis no longer reports the call as having no effect. (Note that Effective_Writes => True is illegal without Async_Readers => True.)
• Changes is volatile (because Async_Writers => True); because Changes does not mutate global state, we are able to set Effective_Reads => False, which allows Changes to remain a function.

This gives us the tools we need to eliminate the nuisance warning on Close and ensure that use of Changes will not be unsound: we are now carrying the necessary information across these FFI subprogram boundaries in our contracts.

The AI agent wasn’t able to get here on its own; I had to work quite a bit with it to reach the point where the model of global state was sufficiently complete and consistent. We’ve enhanced our gnatprove skill (part of AdaCore’s plugin of skills, available here) so that, in the future, AI agents should be more successful at working with abstract global state across FFI boundaries.

Ownership and reclamation of private types

SPARK’s ownership model can be applied to private types, including private types that represent resources living on the other side of the FFI boundary. In memcp, these are things like: the database, prepared statements, and the candle embedder. This not only allows us to ensure a lack of aliasing, but we can annotate the type as needing reclamation.

SPARK requires that a private type to which ownership annotations are applied either have their full view outside of SPARK or contain a type which is subject to ownership.

Typically, when we write bindings, including thick bindings, in SPARK, we write the body in SPARK_Mode => Off; thus it is natural to leave the full view of the private type to which ownership annotations are applied outside of SPARK. In this project, however, since my goal was to get as close to 100% SPARK Silver as possible, I didn’t want to do that: anywhere I had computation, I wanted SPARK_Mode => On.

I solved this problem by introducing another layer of private types (i.e., the fundamental theorem of software engineering applies.) For my Database private type, I introduced a Db_Handle private type like this:

type Db_Handle is private
  with Default_Initial_Condition => Is_Null (Db_Handle),
       Annotate => (GNATprove, Ownership, "Needs_Reclamation"),
       Annotate => (GNATprove, Predefined_Equality, "Only_Null");
--  The C sqlite3*. Owns an open connection until it is closed.

Null_Db_Handle : constant Db_Handle
  with Annotate => (GNATprove, Ownership, "Reclaimed_Value"),
       Annotate => (GNATprove, Predefined_Equality, "Null_Value");
--  The reclaimed value: a Db_Handle equal to this owns nothing, so
--  GNATprove permits dropping or overwriting it.

function Is_Null (H : Db_Handle) return Boolean
  with Ghost, Global => null, Post => Is_Null'Result = (H = Null_Db_Handle);
--  Ghost spelling of "reclaimed", for the Default_Initial_Condition
--  above; executable code compares directly.
--  @param H The handle to test.
--  @return True iff H is the reclaimed value.

The full view looks like this:

pragma SPARK_Mode (Off);

type Sqlite3      is limited null record;
--  Designated type for the C sqlite3. Never allocated or dereferenced on
--  the Ada side: every value comes from SQLite and goes back to it, so all
--  the representation owes us is a pointer comparable to null.

type Db_Handle   is access all Sqlite3;
--  The C sqlite3*, owned until closed; full view a plain C pointer.

Null_Db_Handle   : constant Db_Handle   := null;
--  The reclaimed Db_Handle value: the null pointer.

function Is_Null (H : Db_Handle) return Boolean is (H = null);
--  Completion of the Db_Handle ghost predicate.
--  @param H The handle to test.
--  @return True iff H is the null pointer.

With this machinery in place, I can then say that the C FFI call Close releases the resource:

procedure Close (Db : in out Handles.Db_Handle)
  with Import, Convention => C, External_Name => "memcp_sqlite_close",
        Global => (In_Out => DBMS), Always_Terminates => True,
        Depends => (Db => null, DBMS =>+ Db),
        Post => Db = Handles.Null_Db_Handle;
--  Release the connection and leave Db reclaimed (memcp_sqlite_close, a shim
--  over sqlite3_close_v2 that nulls the caller's pointer). Idempotent:
--  tolerates an already-reclaimed handle.
--  @param Db The connection handle to release; left reclaimed.

Now, as I said above, that postcondition cannot be proved: I have no proof infrastructure on the C side; it’s an assumption that SPARK is told to make about the behavior of the C code. I can review the C and confirm it does as it ought:

/* Close the connection and null the caller's handle. Nulling through sqlite3**
* is what the Ada release postcondition checks at run time under -gnata, and it
* makes Close idempotent: sqlite3_close_v2 (NULL) is a documented no-op.
* close_v2, not close: it tolerates statements not yet finalized, deferring the
* real close until the last one goes. The result code is dropped -- nothing a
* caller could do about it. */
void memcp_sqlite_close(sqlite3 **db) {
 sqlite3_close_v2(*db);
 *db = NULL;
}

Also, I can (and do) test that this works correctly, by building my test suite with -gnata, ensuring that the postcondition is executed and will lead to a (fatal) constraint error if the C code violates its contract.

I then use this Db_Handle type in my Database private type like this:

  type Database is limited private
    with Annotate => (GNATprove, Ownership, "Needs_Reclamation"),
         Default_Initial_Condition =>
           not Is_Open (Database) and then Is_Reclaimed (Database);
  --  Opaque database connection handle.

With full view:

  type Database is limited record
     Handle : Handles.Db_Handle;
     --  The owned sqlite3*; Null_Db_Handle (the default) when not open.
  end record;
  --  Opaque database connection handle.

(There’s the indirection I promised!) Now, SPARK will:

• tell me if I fail to release an object of type Database before it goes out of scope
• not tell me that my calls to Close are without effect.

So my SPARK Silver proof of memcp includes absence of resource leaks for all of the types to which this pattern is applied (Database, Statement, and Embedder).

Unfortunately, the AI agent wasn’t aware of this capability at all. I had to explain how to apply these annotations and how to deal with the restrictions that application of the ownership model imposes. This, too, has been added to our gnatprove skill, to help with future applications of AI agents to this kind of code.

What about CI?

Every PR reproves the whole memcp closure to Silver on Linux, and the gate fails on any unproved check at all. That gate is only useful if people leave it on.

Proof is not cheap. A cold reprove takes about 23 minutes on a GitHub runner; on my machine, it's closer to two minutes. Waiting 23 minutes on every push is the kind of friction that tempts people to ignore the proof gate: eventually someone marks it non-blocking, and then it stops meaning anything.

GNATprove can cache proof results, although the option that does it is confusingly named. --memcached-server accepts either a real memcached daemon or, in the form I use, file:<dir>. A daemon is useless on an ephemeral runner, but a directory can be carried between runs by actions/cache. I’m not aware of anyone else using this in GitHub CI for SPARK today.

There is some risk inherent in using proof caching in CI. Because the cached results are trusted by SPARK, we have to be sure that the cache is accurate and applicable. I do four things to avoid and limit the impact of cache poisoning:

1. The cache key contains a toolchain fingerprint based on the version of gnatprove, why3, and its hash. Moving to a different toolchain means that the cache is no longer found, so a full proof is obtained in every run until a new cache with the new key is written.
2. A nightly job purges all caches, reproves from scratch, and writes a new cache. So even if the cache becomes poisoned, the nightly job will catch potential proof failures and reestablish a clean baseline for the next day. (Depending on the commit cadence, this could be relaxed from daily to weekly.)
3. Only pushes to main and the nightly refresh may write the cache. A branch or a fork PR can read the cache, but can never write it and therefore never poison it.
4. SPARK itself addresses into the cache using verification conditions as keys. This ensures that changes to the code in a commit are reproved, since they modify the verification conditions.

Aside from the proof cache, the proof CI job also skips installing the Rust toolchain, building the Rust libraries (candle has 111 (!) crates in its closure; this takes several minutes to build in CI), and building the Ada code.

On the other hand, CI passes --timeout=10, because --level timeouts are wall-clock rather than step-bounded, and a check that clears on my laptop can time out on a slower runner. SPARK has --replay to replay session files, which include step limits instead of timeouts, but this approach is sufficiently clumsy to use that I avoided it.

The result: 23 minutes cold is reduced to under a minute warm, when there are no new verification conditions. Most PRs, which do have new verification conditions, finish in a few minutes. Cheap enough that nobody is tempted to switch it off.

What about correctness?

You’ve probably noticed that I’ve talked about SPARK Silver (absence of runtime errors) but I haven’t talked about correctness. I took a working Python system and translated it to SPARK; how did I know it was correct? I took a two-pronged approach here, entirely based on testing.

First, early in development, I instrumented the Python code to record tool calls and their results, and used Python memcp as usual for a while. Those real traces turned out to be useless as an oracle: a shared server interleaves sessions, so row IDs drift and history reads legitimately disagree. So the golden corpus had to be synthetic. A generator drove Python through one scripted session against an empty database, with a pinned clock and a deterministic stand-in embedder, and a replay harness in SPARK memcp fed the same requests back in. This was reproducible, and SPARK memcp passed the tests². But a from-empty synthetic corpus can only tell you so much, and for me memcp is "critical infrastructure". I’m truly at a loss trying to use AI agents without it, at this point; my style of working with agents assumes its existence.

So I built my second, and much stronger, approach to correctness testing: I ran SPARK memcp in “shadow” mode alongside the Python memcp. A very thin Python FastMCP server sits in front of the Python memcp and the SPARK memcp; my agents connect to this server and make requests that are forwarded to both Python and SPARK in parallel. Initially, Python’s result was handed back (so Python was the primary and SPARK was the shadow); I’ve now flipped that. Each time this testing server is started, it clones the primary’s sqlite database so the primary and shadow start in lock step. Throughout the run, the shadow’s responses are compared against the primary’s responses; divergences are recorded.

Some divergences were expected (e.g., the candle embedder doesn’t return precisely the same distance scores as sentence-transformers); these are tolerated to a defined epsilon.

But I found two bugs as a result of this testing:

1. Python trims headlines to 100 unicode points; SPARK trims headlines to 100 bytes. Since agents love them some em dashes (confession: so do I, and now I feel like I have to avoid them lest someone accuse me of using an LLM to write for me), SPARK’s headlines are often slightly shorter than Python’s. I deemed this harmless and adjusted the testing system so it doesn’t log these as meaningful divergences.
2. Candle was misconfigured. By default, it was configured to pad all chunks out to 128 tokens before embedding; sentence-transformers did not. So most of the chunks embedded by SPARK were catastrophically different from chunks embedded by Python: the cosine similarity between the embeddings ranged from 0.31 for the small chunks to 0.9 for the medium chunks; the expected result is 1.0. This required a fix and a restart of the testing server (which recloned Python’s database, solving the problem in history). Had I deployed without shadow testing, I would have missed this and the overall performance of memcp would have been significantly degraded.

Why testing and not SPARK Gold (functional correctness)? Gold-level proof is great, but depends on you telling SPARK the properties that it should prove; this is in contrast to Silver, where the proof objectives come from the SPARK language. This makes Gold significantly harder than Silver, although obviously also more interesting.

In high-integrity software development, requirements are typically extremely rigorous; the distance between a requirement and its formalization as a SPARK contract may not be terribly large. For memcp, I’m still struggling to articulate meaningful Gold-level properties that I might want to state and prove (although proven project scoping, a confidentiality property, would be an interesting addition). That’s why I picked a testing-based approach for this work.

What about performance?

Since I’m running the Python and SPARK implementations of memcp in parallel, I can directly compare their performance. The results are striking. First, the memory usage:

I expected SPARK to be more efficient than Python, of course; I didn’t expect SPARK to be 10 times more efficient!

The CPU story is similar, albeit not as striking:

So SPARK is about three times more efficient in CPU use. And on my machine, pytorch is running the embedding model on the GPU and not the CPU; SPARK is running candle’s embedder on the CPU. So that three times is not apples-to-apples, as the embedding computation is effectively removed from the Python row.

What this shows

memcp works, as I declared above. I’m running it “in production” now (i.e., I use it daily as my multi-surface memory for my AI agents). The SPARK Silver proof means that all of the SPARK code is free of runtime errors: no memory safety errors, no arithmetic overflows, no buffer overflows or underflows. Entire classes of potential security errors are provably absent from the SPARK code.

Of course, the Silver proof only exists for the parts in SPARK and depends on the correctness of the boundary annotations, which are necessarily assumptions rather than theorems. That’s why it was worth the effort spent in getting them right.

And memcp demonstrates that SPARK is for more than just embedded code, and that writing a project in SPARK and proving it to Silver is not a huge lift for AI agents. The cost of SPARK used to be that you had to write everything yourself; that cost has moved. Now, the agent handles the volume so you can focus on the boundaries and the critical paths.

I hope you try out memcp and find it brings value to your use of AI agents!

_{¹json-spark is possibly worth a post of its own. A fork of json-ada but with a modified API better fit for SPARK applications,  json-spark 100% SPARK Silver, proves at --level=2 and is immediately useful to anyone who wants to write in SPARK and handle JSON. You’ll find the crate here; I plan to add it to the Alire index soon, so you should be able to alr with json-spark soon, if not already.}

_{²Once the implementation was complete and the golden corpus passed, I deleted it: it was the result of me using AI agents to do stuff on my own machine; I didn’t want it in GitHub. It was also rather large.}