Runtime Verification

Code translation

Make your legacy code migration a security upgrade

Move C, C++, COBOL, Fortran, and Ada to memory-safe, well-supported languages like Rust, Python, and Java, and leave whole classes of vulnerabilities behind.

Differential fuzzing and formal verification check every stage, so the new code keeps the behaviour your business depends on, and none of the bugs.

Plan your migration
Legacy code
  • C
  • C++
  • COBOL
  • Fortran
  • Ada
Rewrite and verifySame behaviour, proven where it matters
  1. 01Specify
  2. 02Rewrite
  3. 03Diff-fuzz
  4. 04Prove
What you ship
  • Safe Rust
  • Python
  • Java
  • Written spec
  • Fuzz harness
  • Formal proofs

Legacy code gets more expensive every year

Harder to staff, harder to change

Fewer engineers know the stack each year, and even a small change needs extensive testing because nobody is sure what else it touches.

Maintenance crowds out new work.

The same bugs keep coming back

In a memory-unsafe language, a buffer overflow is one miscalculation away. The Linux parser we rewrote had two CVEs, sixteen years apart.

A memory-safe language removes the whole class.

Left behind by modern tooling

Dependencies stop getting updates, integrations need workarounds, and AI coding tools work best in the languages they have seen the most of.

Modern languages bring the tools and talent with them.

A safe but incorrect rewrite is useless

Migration is the moment to question the parts of a system nobody has looked at in years. Most rewrites skip it.

Common assumption“Our tests define what the system does.”
RealityTests cover what someone thought to check. Bugs nobody noticed get carried straight across.
Common assumption“The documentation tells us what to preserve.”
RealityDocumentation drifts. Often the code is the only record left of the assumptions the business relies on.
Common assumption“A line-by-line translation is a faithful one.”
RealityLanguages differ on arithmetic, overflow, and error handling. Correct code can become a defective translation.
Common assumption“An LLM can translate it for us.”
RealityIt can produce plausible code quickly. Plausible is not equivalent, and nothing in the output says where it differs.
Common assumption“Rust makes the new code safe.”
RealitySafe Rust removes memory errors, not logic errors. Wrong behaviour in safe code is still wrong.

How it works

Rewrite, then prove it

Differential fuzzing gives empirical confidence. A proof settles it for every input. We use both, and we leave them with you.

Scope a pilot

  1. Specify

    We write down the intended behaviour and security requirements, including the assumptions your team relies on but never documented. Both implementations are checked against it.

    A written specification

  2. Rewrite

    Our engineers translate the code behind the same interface, using LLMs where they speed things up and tagging every deliberate departure from the original.

    A drop-in replacement

  3. Differential fuzzing

    Old and new run side by side on the same generated inputs. Every divergence gets investigated: either the rewrite is wrong, or the original was.

    Evidence of equivalence

  4. Formal verification

    For the properties that matter most, we prove the new code holds them for every input, under explicit assumptions, with proofs checked by K or Lean 4. Nothing AI-generated is trusted without one.

    Mathematical proof

  5. Hand over

    The specification, fuzz harness and proofs live alongside the new code and rerun in CI, so your team can check every future change against them.

    Assurance that lasts

Case study

A Linux kernel parser, from C to safe Rust

The kernel's USB video parser reads untrusted bytes from every camera you plug in, and one of its CVEs was exploited in a phone-unlock chain. We rewrote it in safe Rust, fuzzed the two versions against each other, and machine-checked the property at the heart of CVE-2024-53104.

Along the way the fuzzer surfaced an integer overflow in the original C that could size a frame buffer too small, or at zero. We are now carrying the fix series for the kernel's media maintainers.

Read the full write-up
Linux kernel · CSource
1if (!(format->flags & UVC_FMT_FLAG_COMPRESSED))
2    frame->dwMaxVideoFrameBufferSize =
3        format->bpp * frame->wWidth
4        * frame->wHeight / 8;
Our rewrite · safe RustSource
1if format.flags & UVC_FMT_FLAG_COMPRESSED == 0 {
2    let prod = (format.bpp as u32)
3        .wrapping_mul(frame.w_width as u32)
4        .wrapping_mul(frame.w_height as u32);
5    frame.dw_max_video_frame_buffer_size =
6        prod >> 3;
7}

The fuzzer's one divergence was this line. The product can exceed INT_MAX, which is undefined behaviour in C, so the rewrite now matches the compiled C exactly, and the lasting fix goes into the kernel.

2
CVEs in the original C, sixteen years apart
0
divergences in 54,019 differential executions
93%
edge coverage from the fuzzer
3
patches in the resulting kernel fix series

Built for systems too important to rewrite blind

Start with the component that worries you most. A pilot on one module shows what the full migration will take.

A good fit if you have

  • Business-critical systems written in C, C++, COBOL, Fortran, or Ada
  • A stack that is getting hard to hire for
  • Recurring memory-safety fixes eating into the roadmap
  • Customers or regulators asking for memory-safe code
  • A team that wants AI coding tools to work well on its code
  • A migration already planned, with no way yet to show it preserved behaviour

What you are left with

  • Memory-safe code behind the interface you already have
  • A written specification of the behaviour that matters
  • A differential fuzzing harness comparing old and new
  • Machine-checked proofs of your critical properties
  • Legacy bugs found along the way, with fixes
  • Checks that rerun in CI on every future change

Why Runtime Verification

The engineers behind our Linux C‑to‑Rust work, on your migration

Formal methods since 2010

Our PhD researchers and engineers have been proving critical software correct for NASA, Boeing, and the Ethereum Foundation.

We help build the tools

We contribute upstream to the Rust verification toolchain we use, including Aeneas and Hax, so a gap in the tools gets fixed rather than worked around.

Proven on real code

Our Linux work found a real defect in kernel C, and the fix series is now on the kernel mailing list.

From our research

Read the technical work

Planning a migration? Build the security in from the start

Tell us about your codebase, and we will show you how to move it without losing what makes it work.

Talk to us about your codebase