Semantic Equivalence with the K Framework
One of the most compelling uses for LLM-generated code is migrating legacy code bases. Migrating established code bases needs care: old software is still around because what it does is important, and even with its bugs, it has proven robust enough to survive decades of critical use. When migrating, it's important to keep that track record, bugs included. So it is of the essence that the translated code behaves exactly like the old one. Otherwise, long-standing software systems that depend on the translation being right may just collapse at the worst moment.
So how do we go about it? Tests can only compare the behavior of the original and translated programs on a finite set of inputs, so any behavior outside that set remains unchecked. To guarantee that they match on all inputs, we need formal verification. The usual recipe for formal verification is: given some code and its specification (a description in some formal language of what it ought to do), produce a proof that the code indeed behaves as the spec outlines. Here, the specification of each piece of new code is both executable and precise: behave exactly as the old code did. This turns verification into a relational problem: instead of proving the new code meets a mathematical spec, we prove it behaves like the old code. Code serving as the spec of other code is nothing new; optimized implementations are routinely checked against a simplified reference implementation. Here the reference is the legacy code itself (say, the COBOL payment processing system of your local bank), logic bugs and all. We're not after classical correctness, but proven behavioral equivalence: things keep behaving as they always have, while gaining the niceties of a more modern language (such as memory safety by default, better formal verification tooling, and a wider development talent pool). And if you ever do want functional correctness, you only have to prove it once, on whichever version is easier, and equivalence carries it over to the other.
Proving equivalence is still hard. Differential testing and fuzzing find discrepancies but can't rule them out; translation validation and equivalence checkers can, but none of these approaches is fully automated, and proofs by hand don't scale to a whole code base. And for absolute formal assurance, the proof has to rest on the formal semantics of both programming languages, not on an informal reading of what the code does. That proof is the one formal bridge we need between the old code and the new.
Introducing KEQ, the K EQuivalence prover
That one bridge is what we built KEQ for. KEQ is a semantic equivalence prover based on the K Framework: give it two programs, written in the same language or in different ones, and it proves that they behave the same for all inputs. It has two ingredients: K, which gives us formal semantics for the languages involved, and a language-agnostic equivalence checker (i.e., it works the same whichever languages those are).
The K Framework
The K Framework is the engine that powers most of the formal verification tools developed by Runtime Verification. K can be seen as a programming language for formally defining the semantics of programming languages, and for building automated reasoning tools over those semantics. You write a language's semantics once, in an operational semantics setting, and K gives you tools for that language, such as an interpreter and a symbolic execution engine. Among the languages that have been given semantics in K are Rust's Stable MIR, C, WebAssembly and EVM (the Ethereum Virtual Machine).
The biggest advantage of the K approach is that the same tool can operate over different programming languages by simply plugging in different semantics. In other words, K enables language-parametric formal reasoning tools, and KEQ is one of them.
How KEQ works
Checking that two programs are equivalent is a classical problem in the compiler world, where it goes by the name of translation validation: instead of verifying the compiler once and for all, you check each translation it produces against its input. An LLM migrating your code base can be seen, after all, as a very creative and very untrusted compiler. However, LLM processes cannot (at least as of now) be verified like a traditional compiler can. Hence the need of checking equivalence for code generated with the use of LLMs.
KEQ's checker is a descendant of the algorithm presented in "Language-Parametric Compiler Validation with Application to LLVM", published at ASPLOS '21, whose prototype, also called KEQ, validated a stage of the LLVM compiler on thousands of real-world functions. We refer to the paper for the details of the algorithm, but for understanding the rest of this post it's enough to know that KEQ works in the following two phases.
The first phase is symbolic exploration. KEQ executes each program under its language's K semantics with symbolic inputs: the arguments are variables that stand for every value their type allows. When execution depends on a symbolic expression, such as with if (x > 0), the run splits in two branches. KEQ follows both and, for each resulting path, records the condition the path assumes about the input: x > 0 on one, x <= 0 on the other (for a longer introduction to symbolic execution, see our post Formally Verifying Loops: Part 1). The result of this phase is that we get a graph covering every path through the program. Each graph ends with the value the program returns, written as an expression over the inputs. We call it a KCFG, which stands for K control-flow graph. This phase is the only language-specific part of the job, and all of it comes from each language's semantics.
The second phase is equivalence checking, which works the same regardless of the languages. The inputs for equivalence checking are the KCFGs produced during the symbolic exploration phase, and it matches them to check if their behavior is indeed equivalent. KEQ takes one graph per program, first checks that both programs accept the same set of inputs, and from then on equates the two programs' symbolic inputs. Then it pairs up the paths of the two graphs by the conditions that make them reachable. However, there are a lot of unrelated paths. So a pair of paths that no input could reach together (e.g., x > 0 on one graph, x < 0 on the other) is discarded. For compatible pairs (that is, pairs of paths reached by the same input in both programs) KEQ asks an SMT solver: among the inputs that reach both paths, is there any input on which the two returned values for these paths differ? If all return values agree, the paths agree. If there are disagreeing return values, the input that produced this divergence is a counterexample for equivalence.
The verdict is equivalent when every pair agrees, not equivalent when there is a counterexample (printing such counterexample), and inconclusive when KEQ could not line up the two control flows.
In its current form, KEQ is a prototype, extended from the paper's setting to handle large programming languages outside the compiler setting. It supports C and Rust through our own semantics, so it can check a C program against a Rust program, or two programs written in either one. Supporting any other language takes its K semantics and little work on KEQ's side.
KEQ on small examples
To help visualize the procedure, let's look at KEQ's output on some concrete examples. Take the sign of an integer, in C and in Rust:
int sign(int x) { if (x > 0) { return 1; } else if (x < 0) { return -1; } else { return 0; } }
fn sign(x: i32) -> i32 { if x > 0 { 1 } else if x < 0 { -1 } else { 0 } }
KEQ explores each one and then checks them against each other. This is the output of the check:
C sign (8 nodes, 3 terminal states) 1 ─┬▶ 12 (VAR_x:Int >Int 0) ─▶ 6 returns 1 ├▶ 16 (VAR_x:Int <Int 0 ∧ notBool VAR_x:Int >Int 0) ─▶ 10 returns -1 └▶ 17 (notBool VAR_x:Int <Int 0 ∧ notBool VAR_x:Int >Int 0) ─▶ 11 returns 0 RUST sign (8 nodes, 3 terminal states) 1 ─┬▶ 13 (ARG_INT1:Int >Int 0) ─▶ 7 returns 1 ├▶ 16 (notBool ARG_INT1:Int <Int 0 ∧ notBool ARG_INT1:Int >Int 0) ─▶ 10 returns 0 └▶ 17 (ARG_INT1:Int <Int 0 ∧ notBool ARG_INT1:Int >Int 0) ─▶ 11 returns -1 🔗 C 12 ≡ RUST 13: synced: the same inputs take both branches ✅ C 6 ≡ RUST 7: agree: 1 == 1 ➖ C 12 ≢ RUST 16: vacuous: no input reaches both ➖ C 12 ≢ RUST 17: vacuous: no input reaches both ➖ C 16 ≢ RUST 13: vacuous: no input reaches both ➖ C 16 ≢ RUST 16: vacuous: no input reaches both 🔗 C 16 ≡ RUST 17: synced: the same inputs take both branches ✅ C 10 ≡ RUST 11: agree: -1 == -1 ➖ C 17 ≢ RUST 13: vacuous: no input reaches both 🔗 C 17 ≡ RUST 16: synced: the same inputs take both branches ✅ C 11 ≡ RUST 10: agree: 0 == 0 ➖ C 17 ≢ RUST 17: vacuous: no input reaches both equivalent
Here is how to read it. The output starts with the two KCFGs from symbolic exploration, one line per path: the node ids, the condition the path assumes about the input, in K's notation (VAR_x:Int >Int 0 is x > 0, notBool is negation, ∧ is conjunction, and the Rust side calls its first argument ARG_INT1), and the value the path returns. Three paths on each side, as the source suggests. The two graphs don't list them in the same order, because the intermediate representation of our Rust semantics puts the false branch of a conditional first. However, KEQ only cares about what the path conditions are, not the order they appear in.
Then comes the equivalence check, one line per pair of paths. The symbol 🔗 marks a pair the same inputs can take, say x > 0 on both sides, and the indented line below it reports what the solver said about their return values: ✅ means it proved them equal for every input that reaches both. ➖ marks a pair no input can take at the same time, say x > 0 on one side and x < 0 on the other, so there is nothing to compare. The last line is the verdict, equivalent, in this case.
Now suppose the translation tests the negative case first, which an LLM (or a human) would happily do:
fn sign_reordered(x: i32) -> i32 { if x < 0 { -1 } else if x > 0 { 1 } else { 0 } }
The source has a different shape now, and so does its graph: the path that returns -1 comes first, and the conditions on each path are built from the tests in the new order. None of that matters to the check, because KEQ pairs paths by the inputs that take them, not by where they sit in the graph:
C sign (8 nodes, 3 terminal states) 1 ─┬▶ 12 (VAR_x:Int >Int 0) ─▶ 6 returns 1 ├▶ 16 (VAR_x:Int <Int 0 ∧ notBool VAR_x:Int >Int 0) ─▶ 10 returns -1 └▶ 17 (notBool VAR_x:Int <Int 0 ∧ notBool VAR_x:Int >Int 0) ─▶ 11 returns 0 RUST sign-reordered (8 nodes, 3 terminal states) 1 ─┬▶ 13 (ARG_INT1:Int <Int 0) ─▶ 7 returns -1 ├▶ 16 (notBool ARG_INT1:Int <Int 0 ∧ notBool ARG_INT1:Int >Int 0) ─▶ 10 returns 0 └▶ 17 (ARG_INT1:Int >Int 0 ∧ notBool ARG_INT1:Int <Int 0) ─▶ 11 returns 1 ➖ C 12 ≢ RUST 13: vacuous: no input reaches both ➖ C 12 ≢ RUST 16: vacuous: no input reaches both 🔗 C 12 ≡ RUST 17: synced: the same inputs take both branches ✅ C 6 ≡ RUST 11: agree: 1 == 1 🔗 C 16 ≡ RUST 13: synced: the same inputs take both branches ✅ C 10 ≡ RUST 7: agree: -1 == -1 ➖ C 16 ≢ RUST 16: vacuous: no input reaches both ➖ C 16 ≢ RUST 17: vacuous: no input reaches both ➖ C 17 ≢ RUST 13: vacuous: no input reaches both 🔗 C 17 ≡ RUST 16: synced: the same inputs take both branches ✅ C 11 ≡ RUST 10: agree: 0 == 0 ➖ C 17 ≢ RUST 17: vacuous: no input reaches both equivalent
However, let's see what happens if in Rust x == 0 gave 1 instead of 0:
fn sign_wrong(x: i32) -> i32 { if x >= 0 { 1 } else { -1 } }
A test suite catches this only if someone thought of this edge case. In contrast, KEQ finds it on its own, explicitly pinning the input causing the non-equivalence:
C sign (8 nodes, 3 terminal states) 1 ─┬▶ 12 (VAR_x:Int >Int 0) ─▶ 6 returns 1 ├▶ 16 (VAR_x:Int <Int 0 ∧ notBool VAR_x:Int >Int 0) ─▶ 10 returns -1 └▶ 17 (notBool VAR_x:Int <Int 0 ∧ notBool VAR_x:Int >Int 0) ─▶ 11 returns 0 RUST sign-wrong (6 nodes, 2 terminal states) 1 ─┬▶ 8 (notBool ARG_INT1:Int >=Int 0) ─▶ 6 returns -1 └▶ 9 (ARG_INT1:Int >=Int 0) ─▶ 7 returns 1 ➖ C 12 ≢ RUST 8: vacuous: no input reaches both 🔗 C 12 ≡ RUST 9: synced: the same inputs take both branches ✅ C 6 ≡ RUST 7: agree: 1 == 1 🔗 C 16 ≡ RUST 8: synced: the same inputs take both branches ✅ C 10 ≡ RUST 6: agree: -1 == -1 ➖ C 16 ≢ RUST 9: vacuous: no input reaches both ➖ C 17 ≢ RUST 8: vacuous: no input reaches both 🔗 C 17 ≡ RUST 9: synced: the same inputs take both branches ❌ C 11 ≢ RUST 7: counterexample (VAR_x = ARG_INT1 = 0): 0 vs 1 not equivalent
The Rust side has two paths now, and two of the three pairs the same inputs can take still agree. But the third pair is contradictory: ❌ reports an input (0 in this case) that reaches both ends and gets different answers, 0 from C and 1 from Rust.
However, incorrect translations do not only depend on sound business logic translation. Say the translation decided an int argument was really a count and made it a u32. The two functions can be identical otherwise; KEQ stops before comparing a single path, because the solver finds an input one side accepts and the other rejects:
C echo (3 nodes, 1 terminal states) 1 ─▶ 3 returns VAR_n:Int RUST echo (3 nodes, 1 terminal states) 1 ─▶ 3 returns ARG_UINT1:Int ❌ C 1 ≢ RUST 1: domains differ (VAR_n = ARG_UINT1 = -1) not equivalent
From examples to SHA-256
Small examples are good for illustrative purposes; but we wanted to test KEQ on some real safety-critical code. For that we picked SHA-256, the hash function: the portable C implementation in OpenSSL, whose block function is sha256_block_data_order, and the compact software implementation in the RustCrypto sha2 crate, whose block function is compress. Each takes the running state and one 64-byte block of the message and computes the next state: 64 rounds of additions, rotations and bitwise operations, with the message schedule computed along the way.
We went in steps. First the small bitwise helpers each implementation is built from: KEQ proved each matching pair equivalent, and produced a counterexample when we paired two different ones (OpenSSL's sigma0 against RustCrypto's sigma1). Then one round and one message-schedule step: equivalent too. Then the whole block function, with the incoming state and the block symbolic: no input on which the eight output words differ.
Our C semantics is under heavy development and our Rust semantics is still incomplete, and KEQ's verdicts depend on the semantics being right. Modulo our developing semantics, the SHA-256 experiment shows that the whole pipeline, exploration and checking, holds up on production-ready code from two unrelated and widely used projects, even with different loop structures (OpenSSL partially unrolls the loop, RustCrypto doesn't).
What's next
SHA-256 is one function. We collaborated with the Code Metal formal methods team to inspire and review this work. Next on our list are larger code bases, with many functions calling each other; broader coverage in our semantics for languages like C and Rust, which is what decides how much real code KEQ can take today; and new languages, each one a new K semantics away.
The end goal is the migration from the beginning of this post: an LLM migrates the old code, and KEQ proves the result equivalent to the original. The spec is already written as the old code, and KEQ builds the one formal bridge necessary. Stay tuned to see where KEQ goes to work next!