Migrating C to Ada SPARK with Agentic AI: A Practical Playbook

Safety-critical C codebases typically have a long lifecycle. The development of these code bases is expensive. Most of these code bases are written in C and C++ and this makes them susceptible to a whole host of unintended memory errors. This is why they are carefully written and extensively tested, which both take a lot of calendar time and man-power.

Ada SPARK is a language and formalism that can statically assure the absence of runtime errors and scales up to functional correctness. As such, it can provide a better path to develop and extend these code bases. Agentic AI is a great helper in this as it can enable teams to re-use existing code bases largely as is and carefully decide which parts to translate into Ada SPARK, avoiding whole classes of problems caused by memory errors. The end goal is developing safety critical software faster.

Let me show you what I mean, using the well-known C application curl as an example.

What Is Ada SPARK and Why Does Silver Matter?

Ada is a modern language with all the language features that you expect. Object orientation, generics, concurrency and such. SPARK is a formally verifiable subset of Ada. It strips out Ada features that make formal reasoning hard (dynamic dispatch, exceptions, access types (pointers) in their full generality) and replaces them with a verification model you can actually trust.

SPARK defines several "levels" of verification rigor:

• Stone: Valid SPARK syntax, no formal proof
• Bronze: No uninitialized variables, no illegal aliasing
• Silver: No run-time errors, ever, proven by gnatprove at compile time
• Gold: Functional correctness, proven by contracts
• Platinum: Full formal proof of all properties

Silver is the sweet spot for most safety-critical migration projects. At Silver, gnatprove statically proves the absence of run-time errors, including array out-of-bounds access, integer overflow, and null pointer dereference. This is a class of bug that can impact the safety of a system and that C gives you no protection against.

You don't need to reach Gold or Platinum to get meaningful safety guarantees. Silver alone closes off an entire category of defects that functional safety standards such as DO-178C, IEC 62443, and ISO 26262 address. Moreover, as you reach for Silver for an entire application, critical subprograms at the leaves of the call graph typically need to become more and more golden: you need to be increasingly precise about the promises these critical leaves make to prove the absence of run-time errors in their callers.

Mixing Ada and C in One Binary

You don't have to rewrite everything at once. Ada has first-class C interoperability through its foreign language interface, defined in the Interfaces.C package and the pragma Import / pragma Export mechanisms.

   ada
-- Declare a C function visible to Ada
function curl_easy_init return System.Address
  with Import, Convention => C, External_Name => "curl_easy_init";

Going the other way, you export Ada subprograms to C:

   ada
procedure My_Ada_Handler (data : System.Address; size : Interfaces.C.size_t)
  with Export, Convention => C, External_Name => "my_ada_handler";

The linker doesn't care which object files came from C and which came from Ada. GNAT produces standard ELF objects, and you link them with the same toolchain you already use. This is not a theoretical capability; it ships in every GNAT release and works on bare-metal targets too.

Why LLMs Are Surprisingly Good at This

C to Ada is mechanical in a way that C to Rust is not. Ada's type system, package structure, and subprogram declarations have a close enough correspondence to C constructs that a capable LLM can translate a C file accurately in a single pass most of the time.

The catch is subtle bugs introduced during translation: wrong array index semantics, signed/unsigned mismatches, or a for loop with an off-by-one in the bounds. These bugs are exactly the kind that are hard to spot in a code review but easy to catch with the right feedback signal.

This is where agentic AI earns its keep. A single-shot translation isn't enough. You need a loop:

1. Translate the C file to Ada, including C bindings to replace the original code
2. Compile and surface any GNAT warnings or errors
3. Run the existing test suite against the linked binary, resolve issues found
4. Run gnatprove to check for SPARK Silver violations, resolve issues found
5. Run the existing test suite again, resolve issues found

Each step may have 1 or more iterations that progressively improve the code. The LLM is not just translating; it is responding to a formal verifier and a test harness. gnatprove in particular is a brutally honest feedback source. It either proves the absence of run-time errors or it tells you exactly which line it cannot prove.

The Incremental Migration Playbook

The [curl library](https://github.com/curl/curl) is a good test case. It is a large, well-written, well-tested, real-world C codebase with an established automatic test suite. A partial Ada translation can be found at [ada-curl](https://gitlab.com/mhermeling/ada-curl), which gives you a concrete reference point of the process described in this article.

The migration works file by file, not all at once.

Step 1: Pick a translation unit. Choose a single C file, ideally one with clear boundaries and limited global state. curl/lib/base64.c is a clean starting point: no network I/O, pure functions, straightforward logic. Usually, this will be a leaf in the call graph.

Step 2: Translate to Ada. The LLM converts the file to an Ada package. Types map to Ada types, functions map to subprograms, #define constants become Ada constants or named numbers.

Step 3: Write C wrappers. The LLM generates thin C wrappers around each exported Ada subprogram. The rest of the C codebase calls the wrappers, not the Ada code directly. This keeps the changes to the rest of the codebase minimal.

   c
// Auto-generated C wrapper
int base64_encode(const char *input, size_t in_len, char **output, size_t *out_len) {
    return ada_base64_encode(input, in_len, output, out_len);
}

Step 4: Update the build system. The LLM adds gprbuild or gnatmake as a step in the existing CMake or Makefile build. The Ada objects land in the same link step as everything else.

   makefile
ada_objects:
    gprbuild -P ada_curl.gpr

libcurl.a: ada_objects $(C_OBJECTS)
    ar rcs $@ $(C_OBJECTS) $(ADA_OBJECTS)

Step 5: Run the test suite. curl's test suite is extensive. If the translated unit passes the same tests the C version passed, the translation is behaviorally equivalent. Any failure goes back into the agentic loop. The LLM can run this repeatedly and fix issues as needed.

Step 6: Lift to SPARK Silver. The LLM adds the SPARK_Mode => On annotation and, with Pre and with Post contracts where gnatprove demands them, and run the prover. Violations are precise: the prover tells you which line, which check, and why it cannot discharge it. We’re working on an agent Skill (SKILL.md and associated supporting resources) that largely automates this process; stay tuned for more on this soon.

Step 7: Run the test suite again. Step 6 may have modified the code slightly, an automated re-run of the test suite verifies that nothing has been invalidated. Again, something that the LLM can do and in case there are any problems, fix the problems, while keeping the file marked as SPARK Silver.

Repeat this for each file. Over time, the Ada surface area grows, the C surface area shrinks, and the verified codebase expands incrementally without ever breaking the build.

Not All Code Is A Candidate

Code that is heavy in memory manipulation or that uses function pointers can be difficult to translate in an automated fashion by an LLM. This is not to say that the code cannot be converted into SPARK, just that standard LLM driven translation has its limits in translating these patterns and needs more human guidance.

An LLM is a tool; it is not a software engineer. Before embarking on the translation of an entire project, a software engineer or architect should look at the C code and decide what the business value of a translation is. Interestingly, LLMs can assist with this investigation as they can quickly generate a summary of the codebase. A diagram of the curl structure is provided at the end of this article to visualize the pieces where the LLM believes it can perform automated translation and which pieces need human assistance.

Help the LLM

The field of AI and LLMs is rapidly evolving, with new releases coming out almost weekly. One of the more recent additions is the Agent Skills specification. A skill helps guide an agent through a particular task and provides hints for the agent to use. In the case of C to SPARK translation, a hint could be how to deal with floating points, how to speed up proving a loop, debugging a failed proof, or hard-won lessons from previous translations.

A skill can also drive the agent to write a summary for every file translated. See the end of this article for an example of a summary for the translation of dict.c.

The Quality Of The Code

The translated code will be valid SPARK code and be free from run-time errors; the unit tests pass, so all is well. However, it is not ‘proper’ SPARK code; it is not code that a software engineer would have written from scratch using SPARK, especially in the sense of the usage of types.

See, Ada and SPARK are type safe languages. You would create a type for everything. Instead of using ‘float’ for a variable Temperature, which could be either Fahrenheit, Celsius, or even Kelvin, a developer in Ada would create a type Temperature_in_Fahrenheit based on Float and use that in the program, further clarifying the use of the type and the variable and preventing type confusion.

It is up to the user then to either leave the code as is or do another pass through the source code to uplevel the usage of proper types. Any new code that gets added should absolutely use the Ada type system and let the compiler help protect the developer from type confusion problems. Our Skill emphasizes this; subtype creation is a key element of the workflow the agent is instructed to follow as it raises SPARK code to SPARK Silver.

What It Actually Costs

A single C file of 200-500 lines takes an agentic pipeline roughly 10-30 minutes of wall-clock time and a few cents in API costs, depending on the model and the number of iteration cycles. A codebase the size of curl's core, around 150,000 lines of C, would take weeks of compute time running continuously, but the human effort is mostly in setup, reviewing SPARK contracts, and handling the edge cases the LLM flags for human review. This is not a weekend project, but it is not a multi-year rewrite either.

Where This Leaves You

SPARK Silver gives you machine-checked proof obtained during build time that runtime errors cannot occur in the translated code. The incremental approach means you never break the build, and you validate every step against your existing tests. Agentic AI turns what was previously an expert-only, manual process into something a small team can drive in a short timespan.

The takeaway from this article is that a) you can cheaply (in effort and time) convert pieces of an existing code base to Ada without breaking functionality, and b) you can build new functionality on top of your existing code base using a memory safe language.

All the tools involved are open source: GNAT, gnatprove, and Alire, the package manager, ship under GPL with a runtime exception. Commercial support is available from companies like AdaCore, which support the tooling, and can provide certification artifacts for DO-178C, ISO 26262, and similar standards for projects where you need it.

If you are shipping safety-critical software and you are still relying on C's lack of run-time guarantees, it is worth running a small proof-of-concept against your own codebase. Pick one file, stand up the LLM pipeline, and see for yourself how easy it is to convert your C code to Ada and benefit from the memory safety and the absence of run-time errors.

Curl Architecture and SPARKability

The diagram below shows which functions were converted and provides suggestions as to what components to tackle next and what components require a redesign before tackling.

╔══════════════════════════════════════════════════════════════════════════════╗
║                         libcurl Architecture                                 ║
║                                                                              ║
║  Legend:  [✓] Ada/SPARK done  [~] SPARK candidate  (blank) = redesign needed ║
╚══════════════════════════════════════════════════════════════════════════════╝

┌─────────────────────────────────────────────────────────────────────────────┐
│  PUBLIC API                                                                 │
│  easy.c  ·  multi.c  ·  setopt.c  ·  getinfo.c  ·  curl_share.c             │
└────────────────────────────────┬────────────────────────────────────────────┘
                                 │
┌────────────────────────────────▼────────────────────────────────────────────┐
│  URL / SETUP                                                                │
│  url.c  ·  urlapi.c  ·  connect.c  ·  conncache.c                           │
└──────┬─────────────────────────────────────────────────────────────┬────────┘
       │                                                             │
┌──────▼───────────────────────────────────────────┐   ┌───────────▼────────┐
│  TRANSFER ENGINE                                 │   │  DNS RESOLUTION    │
│  transfer.c  ·  request.c  ·  sendf.c            │   │  hostip.c          │
│  multi_ev.c  ·  select.c   ·  progress.c         │   │  asyn-ares.c       │
└──────────────────────┬───────────────────────────┘   │  asyn-thrdd.c      │
                       │                               │  doh.c             │
┌──────────────────────▼───────────────────────────────┴────────────────────┐
│  CONNECTION FILTER CHAIN  (cfilters.c — vtable hub)                       │
│                                                                           │
│   ┌──────────────┐  ┌─────────────────┐  ┌──────────────┐                 │
│   │  cf-socket.c │  │  cf-ip-happy.c  │  │  cf-h*proxy  │                 │
│   │  (raw I/O)   │  │  (happy eyeballs│  │  cf-haproxy  │                 │
│   └──────────────┘  └─────────────────┘  └──────────────┘                 │
│                                                                           │
│   ┌──────────────────────────────────────────────────────────────────────┐│
│   │  TLS LAYER  (vtls/vtls.c — backend vtable)                           ││
│   │  openssl.c · gtls.c · mbedtls.c · wolfssl.c · schannel.c · apple.c   ││
│   │                                                                      ││
│   │  vtls/hostcheck.c [~]  ·  vtls/cipher_suite.c [~]                    ││
│   │  vtls/x509asn1.c       ·  vtls/keylog.c                              ││
│   └──────────────────────────────────────────────────────────────────────┘│
│                                                                           │
│   ┌──────────────────────────────────┐                                    │
│   │  QUIC  (vquic/vquic.c)          │                                     │
│   │  curl_ngtcp2.c · curl_quiche.c  │                                     │
│   └──────────────────────────────────┘                                    │
└───────────────────────────────────────────────────────────────────────────┘
                       │
┌──────────────────────▼──────────────────────────────────────────────────────┐
│  PROTOCOL HANDLERS  (each registers a Curl_handler vtable)                  │
│                                                                             │
│  HTTP family                    Mail/Other                   File/Special   │
│  ┌────────────────────────┐    ┌─────────────────────┐    ┌───────────────┐ │
│  │ http.c  ·  http1.c     │    │ smtp.c  · pop3.c    │    │ file.c        │ │
│  │ http2.c  [✓ partial]   │    │ imap.c  · ftp.c     │    │ dict.c  [✓]   │ │
│  │ http_chunks.c          │    │ mqtt.c  · telnet.c  │    │ gopher.c      │ │
│  │ http_proxy.c           │    │ ftplistparser.c     │    │ tftp.c        │ │
│  │ http_aws_sigv4.c       │    │ rtsp.c  · smb.c     │    │ ws.c          │ │
│  │ http_digest.c          │    └─────────────────────┘    └───────────────┘ │
│  │ http_ntlm.c            │                                                 │
│  └────────────────────────┘                                                 │
│                                                                             │
│  SSH (vssh/)                    HTTP Metadata                               │
│  ssh.c · libssh2.c · libssh.c   headers.c · cookie.c · hsts.c · altsvc.c    │
└─────────────────────────────────────────────────────────────────────────────┘
                       │
┌──────────────────────▼──────────────────────────────────────────────────────┐
│  AUTH SUBSYSTEM  (vauth/vauth.c — function pointer dispatch)                │
│                                                                             │
│  basic.c  ·  oauth2.c  ·  cram.c  ·  cleartext.c                            │
│  digest.c      (uses curl_maprintf, dynbuf — not SPARK-able)                │
│  ntlm.c   ·  krb5_gssapi.c  ·  spnego_gssapi.c                              │
└─────────────────────────────────────────────────────────────────────────────┘
                       │
┌──────────────────────▼──────────────────────────────────────────────────────┐
│  CRYPTO PRIMITIVES                                                          │
│                                                                             │
│  ┌─────────────────────┐   ┌───────────────────┐   ┌─────────────────────┐  │
│  │ md5.c       [✓]     │   │ sha256.c          │   │ hmac.c              │  │
│  │ md4.c       [✓]     │   │ curl_sha512_256.c │   │ (fn ptr + malloc)   │  │
│  │                     │   │          [✓]      │   └─────────────────────┘  │
│  └─────────────────────┘   └───────────────────┘                            │
│                                                                             │
│  vauth/digest_hex  [✓]   ·   curl_ntlm_core.c  (DES via OpenSSL)            │
└─────────────────────────────────────────────────────────────────────────────┘
                       │
┌──────────────────────▼──────────────────────────────────────────────────────┐
│  I/O BUFFERING                                                              │
│                                                                             │
│  bufq.c  [✓ Ada, proof pending]   ·   bufref.c   ·   content_encoding.c     │
│  dynhds.c  ·  mime.c  ·  formdata.c                                         │
└─────────────────────────────────────────────────────────────────────────────┘
                       │
┌──────────────────────▼─────────────────────────────────────────────────────┐
│  DATA STRUCTURES & UTILITIES                                               │
│                                                                            │
│  Pure (strong SPARK candidates):                                           │
│  ┌────────────────────────────────────────────────────────────────────────┐│
│  │ splay.c         [~]  splay tree — pure pointer manipulation            ││
│  │ curl_endian.c   [~]  endian byte-swap — trivial bit arithmetic         ││
│  │ strcase.c       [~]  case-insensitive compare/convert — pure char ops  ││
│  │ strequal.c      [~]  string equality — pure                            ││
│  │ uint-bset.c     [~]  bit set — pure bit arithmetic                     ││
│  │ uint-spbset.c   [~]  sparse bit set — pure                             ││
│  │ parsedate.c     [✓]  date parsing — pure (no I/O or alloc)             ││
│  │ curl_fnmatch.c  [~]  glob pattern match — pure algorithm               ││
│  │ curlx/base64.c  [✓]  base64 encode/decode — pure transformation        ││
│  │ escape.c        [~]  URL encode/decode — pure (output needs malloc)    ││
│  └────────────────────────────────────────────────────────────────────────┘│
│                                                                            │
│  Allocating (malloc-heavy, not SPARK-able as-is):                          │
│  hash.c  ·  llist.c  ·  slist.c  ·  uint-hash.c  ·  uint-table.c           │
│  curlx/dynbuf.c  ·  mprintf.c  ·  curlx/strdup.c                           │
└────────────────────────────────────────────────────────────────────────────┘

╔═════════════════════════════════════════════════════════════════════════════╗
║  SPARK SUMMARY                                                              ║
║                                                                             ║
║  [✓] Done (9 units, 0 unproved):                                            ║
║      md5, md4, sha512_256, digest_hex, http2_ada (partial), buf_queue       ║
║      dict, base64, parsedate                                                ║
║  [~] Best next candidates (pure computation, no OS/malloc/vtable):          ║
║      1. curl_endian.c  — ~50 lines of bit-swap, trivial to prove            ║
║      2. strcase.c      — character table lookup, ideal for SPARK            ║
║      3. curl_fnmatch.c — glob matching FSM, no alloc                        ║
║      4. splay.c        — tree rotations, bounded by tree depth              ║

║                                                                             ║
║  Redesign needed: anything touching sockets, TLS backends, vtable dispatch, ║
║  curl_maprintf, Curl_safefree, dynbuf, or external libraries (nghttp2,      ║
║  OpenSSL, GSSAPI).                                                          ║
╚═════════════════════════════════════════════════════════════════════════════╝

proof-status-dict.md

Proof Status: Dict_Ada (lib/dict_ada.ads + lib/dict_ada.adb)

Unit fully proved at level 2, mode all (--quiet, no check messages). Only flow-analysis warnings remain (unused initialisers on locals — not proof issues).

Proved

[x] To_Upper (level 2, expression function — no obligations)

[x] Needs_Escape (level 2, expression function — no obligations)

[x] CI_Starts_With (level 2)

   [x] index check Path(Path'First+I) — loop invariant + pre restructure

   [x] index check Pref(Pref'First+I) — loop invariant

   [x] preconditions at Classify call sites — pragma Assert after Path_Len=0 guard

[x] Classify (level 2)

   [x] preconditions for all CI_Starts_With calls — early return + explicit asserts

[x] Find_Colon (level 2)

   [x] index check Path(I) — added From>=Path'First to precondition + loop invariant

   [x] postcondition Result>=From and Result<=Last+1 — loop structure

[x] Append (level 2)

   [x] overflow Pos+Len — two-step check (Len>Req_Max, then Pos>Req_Max-Len)

   [x] index checks Buf(Pos+I), Src(Src'First+I) — loop invariants

[x] Append_Byte (level 2)

   [x] index check Buf(Pos) — guard Pos>=Req_Max

[x] Unescape_Word (level 2)

   [x] underflow Input'Length-1 — early return guard for empty input

   [x] index check Input(Input'First+I) — loop invariant

   [x] overflow O (escape case) — loop invariant O<=2*I, assert O<=Esc_Max-2

   [x] postcondition Out_Len<=Esc_Max — from loop invariant + Word_Max bound

[x] Build_Request (level 2)

   [x] overflow Path'Length in precondition — nested or-else guard

   [x] overflow Client'Length in precondition — same pattern

   [x] W/D/S_Start>=Path'First — pragma Assert chain from Find_Colon postcondition

   [x] slice Esc(0..Esc_Len-1) — Unescape_Word postcondition Out_Len<=Esc_Max

C-export Wrappers (SPARK_Mode Off — not subject to proof)

[x] C_Unescape_Word (dict_ada_unescape_word)

[x] C_Build_Request (dict_ada_build_request)

Key Design Decisions

• Preconditions use nested or else to avoid evaluating 'Length when 'Last = Natural'Last would overflow: Len=0 or else (Src'Last <
• Natural'Last and then Len <= Src'Length). See overflow-patterns.md. CI_Starts_With requires Path'Last < Natural'Last unconditionally so the prover has a direct fact without case splitting across the disjunction.
• Classify has an early if Path_Len = 0 then return Cmd_Bad plus explicit pragma Assert to make Path'Last<Natural'Last directly available to callers.
• Find_Colon precondition requires From >= Path'First (when From <= Last) to make index check Path(I) provable directly from loop bounds.

Subtype Debt

The constraint X'Last < Natural'Last appears in 5+ preconditions. A subtype encoding this bound would eliminate the repetition. Not introduced due to time; consider for a future refactor. See contracts.md "Subtype Self-Check".