Dante: A Case Study in Compiler-Assisted Verification Using Model Checking

Introduction

If you're a developer today, chances are you've experienced the “magic” of LLMs in your workflow, whether you realize it or not. That auto-completion in your JetBrains IDE, Visual Studio, or Cursor? There's cases where an LLM working behind the scenes, either locally or in the cloud, making your coding experience smoother.

The exciting part is that LLMs are doing much more than just completing your code. They're helping with refactoring, optimization, and all sorts of code transformations that used to take hours of manual work. But here's where things get interesting—and a bit concerning. While these AI-powered transformations are incredibly useful, they're not infallible. Just like us humans, LLMs can introduce subtle bugs when refactoring code, similar to how we might make mistakes when writing LLVM optimization passes or crafting Roslyn analyzers causing wrong transformations.

This creates a challenge: how do we harness the power of automated code transformations while being certain they don't break our code? The answer lies in Formal Equivalence Checking—a way to mathematically prove that transformed code behaves identically to the original.

Overview

At its core, Dante compiles C# to Z3 formulas, then Z3 (the SMT solver) solves the generated satisfiability problem. The compilation pipeline works as follows:

C# Frontend Processing handles lexing, parsing, and semantic analysis using Roslyn, Microsoft's C# and VB compiler.

Compile C# CFG to Z3 is where the core compiler comes into play, including liveness dataflow analysis, compiling CFG operations from Roslyn's bound tree to Z3 equivalent operations using appropriate theories, lambda calculus beta reduction to model variable state mutation within basic blocks, and generating the bi-proposition between the two compiled programs. Basic blocks become Z3 recursive functions in functional SSA form.

Solve the Formulas is where the SMT solver attempts to solve the bi-proposition, trying to find values that break it. SAT means A ≠ B (transformation error), UNSAT means the transformation is correct, and UNKNOWN means the problem is undecidable within finite time and resources.

Inside The Compiler

The compiler progresses through four main phases, which I'll explain in detail.

Dataflow Analysis

This first compilation phase helps generate Z3 formulas in functional SSA form. Unlike typical SSA construction (dominator tree → dominator frontier → Phi insertion → value renaming), Dante takes a different approach for efficiency.

When performing liveness analysis, you typically need foundational sets like Defs(B), Uses(B), and UpwardExposed(B). Roslyn provides sets similar to these, but Dante uses 'DataFlowIn' (UpwardExposed)—the set of local variables that are used in a region but may be defined or written outside of it. Essentially, if variables are dead du to redefinition (as in SSA form define), they won't be part of this set, allowing us to compute symbol liveness directly. Since Roslyn's dataflow analysis is region-based so it could span multiple basic blocks (the span of blocks form a super basic blocks aka single entry multiple exit blocks), the liveness analyzer matches regions to basic blocks and computes live-in/live-out sets.

The pass consists of Partial Liveness Analysis (processing a DAG by computing symbols alive at basic block boundaries, excluding back edges) and Complete Liveness Analysis (handling loops by joining partial liveness sets with loop header liveness).

This approach is conceptually similar to B. Boissinot and F. Rastello's work.

When constructing functional SSA and generating basic blocks as functions, you need to know which symbols the basic block and its successors require—these are the live-in symbols. Using dataflow analysis for SSA construction is well-studied (see D. Das et al.), though Dante's algorithm differs from their approach.

The result is a "pruned" SSA program where basic block parameters act as Phi nodes (when blocks join) or fall-through symbols (in sequential cases). Since only live symbols can be declared as parameters, there are no dead phi nodes by definition.

State Mutation

In languages like C#, C++, and Java, symbols are mutable by default. This raises a question: how do you express mutation in an immutable target?

One approach is creating a function wherever you find an assignment:

int Function(int x, int y)
{
    x += 10;
    y *= x + 50;
    return x / y;
}

In SMTLIB2, this becomes:

(define-fun Function ((x Int) (y Int)) Int (/ x y))
(define-fun MutateY((x Int)(y Int)) Int (Function x (* y (+ x 50))))
(define-fun MutateX((x Int) (y Int)) Int (MutateY (+ x 10) y))

Each statement becomes a function where new versions of symbols get passed as arguments. This works but creates numerous functions—imagine a program with 10 functions, each with 20 branching statements.

Dante handles this more elegantly using lambda calculus beta reduction:
Example: (λx.x+1) 5 →β 5+1
General rule: (λx.M) N →β M[x:=N], where M[x:=N] means substitute all free occurrences of x in M with N
For the compiler, each symbol is a function and each use is an application. Instead of state transfer, the compiler reduces symbol values at each use point:

(define-fun Function ((x Int) (y Int)) Int
    (/ (+ x 10) (* y (+ (+ x 10) 50)))
)

Notice how 'x' was reduced twice to (+ x 10). Z3 performs common subexpression elimination and represents expressions as a DAG through hash consing, so nodes get reused efficiently.

internally the compiler will treat each variable re/assignment as a new definition and will use the immediatly dominating definition in later operations in basic block, this essentially similar to SSA variable renaming where latest version of a variable dominates other definitions, the following code demonstrate how the compilers (conceptually) treat state mutation in same basic block

int Function(int x0, int y0)
{
    x1 = x0 + 10;
    y1 = y0 * x1 + 50;
    return x1 / y1;
}

Ultimately, both approaches—separate mutation functions versus beta reduction—converge to similar DAG representations in the SMT solver, since interpreted or non-abstract functions act as syntactic sugar over the underlying expressions that Z3 processes.

In Z3 and SMT solvers generally, functions are pure and total, meaning they have no side effects and are defined for any argument in their domain.

Control Flow Graph Code Generation

Dataflow analysis and beta-reduction are the cornerstones for generating Z3 code. The 'Function' code generator visits basic blocks in depth-first fashion. For each basic block, the 'Expression' code generator generates the operations within basic blocks.

Assignment expressions are treated as functions that return the RHS (right-hand side) of the expression. When the L-Value expression (the LHS or left-hand side of the assignment) gets referenced, it gets reduced to its RHS expression tree—essentially the beta-reduction we discussed earlier.

Several special operations require special handling besides assignment operations, such as 'FlowCapture' and 'FlowCaptureReference' operations. LINQ is essentially a collection of operations (Map aka Select, Filter aka Where, etc.) over a sequence monad 'IEnumerable', and many of these are higher-order functions requiring special support.

Why Special Support for Higher-Order Functions? SMT solvers are designed to provide decision procedures that terminate with definitive answers. Higher-order logic is generally undecidable—there's no algorithm that can determine in finite time whether an arbitrary higher-order formula is satisfiable. SMT solvers handle first-order logic only, but some solvers like Z3 have limited support for higher-order logic, including limited support for quantification over functions, which the compiler utilizes elegantly.

Bi-Proposition Generation

The final step generates the bi-proposition expression that the solver will assert against. The assertion essentially asks: "Find any value that breaks the bi-proposition."

• If the solving result is SAT, then the transformation from program A to program A' contains an error

• If the result is UNSAT, then the transformation is correct

• If the result is UNKNOWN, then it's an undecidable problem

Here's a simple example:

public bool Original(int lhs, int rhs)
{
     return lhs <= rhs;
}

public bool Transformed(int lhs, int rhs)
{
     return rhs >= lhs;
}

After code generation:

(declare-fun param!1 () Int)
(declare-fun param!0 () Int)
(define-funs-rec ( ( BB1000 ((x!1 Int) (x!2 Int)) Bool)
                   ( BB1001 ((x!1 Int) (x!2 Int)) Bool)
                   ( BB0000 ((x!1 Int) (x!2 Int)) Bool)
                   ( BB0001 ((x!1 Int) (x!2 Int)) Bool))
                 ( ((_ BB1001 0) x!1 x!2)
                   (>= x!2 x!1)
                   ((_ BB0001 0) x!1 x!2)
                   (<= x!1 x!2)))
;the Bi-Proposition mentioned earlier
(assert (not (= ((_ BB0000 0) param!0 param!1) ((_ BB1000 0) param!0 param!1))))

Output:

original function always implies transformed function; there was no set of values that could be assigned to the abstract symbols that would break the bi-proposition.

LINQ and Higher-Order Functions

Let's explore how Dante handles LINQ with a simple example:

public IEnumerable<int> TransformedTakeAndFilter(int[] numbers)
{
    return numbers.Take(10).Where(n => n > 10 && n < 30);
}

The compiler detects LINQ expressions and processes each method recursively. For higher-order functions like 'Where', it generates the lambda expression as a Z3 function and builds an intermediate expression tree.

The Array Theory Challenge: Dante represents IEnumerable as arrays, but arrays in SMT are infinite while our data is finite. Z3's array theory is based on the axiom of extensionality and two core axioms: Select (storing then selecting from the same index returns the stored value) and Store (storing at one index doesn't affect other indices).

Dante solves this by marking invalid positions with impossible values. For Take(10), all positions from index 10 onward get marked with int.MaxValue + 1 (impossible in C# but valid in Z3's infinite integers). For 'Where', the compiler creates a map storing invalid values where the predicate returns false. For 'Select', it uses Z3's map axiom where selecting from a mapped array applies the function to the original element.

Query Building: LINQ operations can't be processed independently—sometimes they need reordering or injection of predicates into functors (like Select(...).Where(...)). The compiler builds queries lazily then generates proper Z3 code based on context.

Generics: Since Z3 doesn't support generic types, Dante performs monomorphization with simple name mangling for types and functions.

Limitations

I want to address some limitations worth mentioning. Partial Bounded Model Checking is one key limitation—verifying code with loops and recursion can continue indefinitely because it's unbounded. The solver will try to solve formulas with recursive nature indefinitely, relative to the domain of values used to terminate recursion. With bounded model checking, one can define the maximum depth for recursion so the solver can reason about a finite range of recursive calls (you can check projects like CBMC).

Personal Note

This project holds special significance as it was written as a tribute to my son Dante ❤️—a symbol of the love and inspiration that drives meaningful work.