Design Space 05: Verification

Series: AI-Native Programming Language Research — Design Space Memos Document 5 of 6 (planned: shapes, AD-through-effects, sparsity, distribution, verification, hardware abstraction)

1. Problem statement

ML compilers perform enormous semantic transformations on programs. A modern training graph goes through, at minimum:

• Reverse-mode AD (rewrites the program to compute gradients).
• Operator fusion (combines kernels).
• Layout transformation (NCHW ↔ NHWC, blocked layouts).
• Quantization (changes the numerical type with bounded error).
• Sharding propagation (rewrites tensors and inserts collectives).
• Polyhedral tiling, loop interchange, and reordering.
• Memory planning and reuse.
• Final code generation to LLVM, PTX, SPIR-V, or vendor IRs.

Each transformation can be wrong, and most have no proof of correctness. The ecosystem manages this with extensive regression testing, numerical tolerance checks, and gradcheck-style validation. This catches most bugs but has well-known failure modes: silent gradient errors that converge slowly or to wrong solutions; sharding inconsistencies that surface only at scale; fusion miscompiles that are correct on small inputs and wrong on large ones; quantization error accumulation that's invisible until a downstream task degrades.

The state of the art for traditional compilers is much better. CompCert (Leroy, 2006–) is a verified C compiler — every optimization pass has a Coq proof of semantic preservation. CakeML (Kumar et al., 2014–) is a verified compiler for an ML-family language (the programming-languages ML, not the field). seL4 (Klein et al., 2009) is a verified microkernel. The Project Everest stack (HACL*, EverCrypt, miTLS, F*) verifies cryptographic implementations. The methodology is mature; the cost is high but bounded; the results are durable.

No equivalent exists for ML compilers. There are pieces — verified AD calculi for restricted languages, verified linear algebra kernels for small cases, neural-network property verifiers like Reluplex — but no end-to-end verified ML compilation pipeline, and no production-grade verified subset.

This memo: maps what needs verification, surveys what exists, identifies the most achievable targets, and argues that verified compilation passes are the single most concretely achievable research contribution in this whole design-space series. The methodology is well-understood, the existing partial results are real, and the production demand (correctness at scale) is increasing as model sizes grow.

For someone with a formal-methods background — Frama-C work, an eBPF verifier, refinement-typed kernel libraries — this is the memo where the design space turns into a tractable research program rather than a survey.

2. What needs to be verified in an ML compiler

A taxonomy by transformation, with rough difficulty estimates:

The pattern: transformations that are essentially algebraic (sharding, layout, AD on a clean core) are tractable. Transformations that involve concurrency, floating-point, or unbounded composition are genuinely hard.

The order of attack should be the tractable ones first, building up the framework before tackling the hard ones.

3. Verification approaches

Five distinct methodologies, each with established communities and tooling.

3.1 Proof assistants (Coq, Lean 4, Isabelle/HOL, Agda)

The heaviest and most rigorous. You write definitions, theorems, and proofs in a dependently-typed language, and the kernel of the proof assistant checks every step. This is what CompCert, seL4, and the four-color theorem use.

For ML verification: Coq has Coquelicot for real analysis and MathComp for linear algebra. Lean 4 has mathlib and is gaining ML-specific libraries. Both have working AD formalizations for restricted languages.

Cost: very high. Proof-to-code ratios of 5:1 to 20:1 are typical. Proofs require mathematical maturity and tooling familiarity that takes months to acquire.

Where it's worth it: core compiler passes that will be reused thousands of times. CompCert is the model: prove once, compile forever.

3.2 SMT-augmented verification (F*, Dafny, Why3)

Lighter-weight: you write specifications in a verifier-friendly language, and an SMT solver (Z3, CVC5) discharges most obligations automatically. You write proofs only where the SMT solver gives up.

For ML: F* powers Project Everest's verified cryptography. Dafny is used in distributed systems verification. Why3 (and its Coq backend) is the standard for verified numerical computation (Boldo, Filliâtre, Melquiond).

Cost: lower than proof assistants — proof-to-code ratios of 1:1 to 3:1. SMT timeouts are the operational pain point.

Where it's worth it: numerical bounds, simple semantic preservation, contracts on data structures. Quantization error analysis in particular fits this style.

3.3 Refinement types (Liquid Haskell, LiquidJava, Granule)

Lightweight: types are augmented with predicates over their values, and an SMT solver discharges the predicates at type-checking time. The user gets static guarantees without writing explicit proofs.

For ML: the entire previous four memos pointed at refinement-typed tensors. Refinement types on tensor shape, sparsity pattern, and sharding are exactly the static guarantees we want, and they cost roughly an annotation per function rather than a proof.

Cost: low — comparable to writing types in a normal language. SMT decidability is the binding constraint on what predicates you can express.

Where it's worth it: the surface language. Refinement types on tensors are the right user-facing verification level; heavier methodologies sit underneath, hidden from users.

3.4 Rust-family verifiers (Verus, Creusot, Prusti, Aeneas)

A new and rapidly maturing class: take Rust's borrow checker as the foundation (which already gives you safe aliasing and memory safety), and layer functional verification on top. Verus (Lattuada et al.) compiles Rust + specifications to SMT. Creusot translates to WhyML. Aeneas translates to a pure functional language for proving in Coq/Lean.

For ML: Mojo is partially Rust-influenced; PyTorch has expanding Rust internals; Apple MLX has Rust components; the Hugging Face Candle library is Rust-native. There is a credible path where the AI-native language's implementation is verified Rust, even if its surface language is something else.

Cost: medium, with low marginal cost since Rust's type system already does half the work. The Rust verification community is the most active formal-methods area outside academic strongholds right now.

Where it's worth it: verified runtime systems (memory planners, schedulers, allocators), verified kernels at the language level, and verified compilation passes implemented in Rust.

3.5 Translation validation

Instead of proving the compiler correct, prove each run of the compiler correct: take the input program and the output program, generate a verification condition that says they're equivalent, and discharge it with an SMT solver.

For ML: Alive2 does this for LLVM. Translation validation for ML compilers is an obvious direction with very little published work.

Cost: low marginal cost per run (SMT discharges automatically when it can), but no general guarantee. Hard cases require manual intervention.

Where it's worth it: compilers under active development where the source code changes faster than proofs can be updated. Most ML compilers are in this regime.

4. Existing work in verified ML

The literature is sparse but real. Three threads worth knowing:

4.1 Verified AD

The most developed area. Brunel, Mazza & Pagani (POPL 2020), "Backpropagation in the Simply Typed Lambda-Calculus with Linear Negation," gives a typed reverse-mode AD calculus with a proof of correctness. The setting is restricted (simply typed lambda calculus, no effects), but the proof technique generalizes.

Krawiec et al. (POPL 2022), "Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode AD," extends this to higher-order programs and proves an asymptotic-efficiency bound (the AD cost is within a constant factor of the primal cost). This is the closest existing work to "verified AD as a compiler pass."

Smeding & Vákár (POPL 2024), "Efficient CHAD" and related work, push toward a verified production-quality AD. Mazza & Pagani have several follow-up papers on differential lambda calculus.

What's missing: verified AD over a language with effects (memo 2's framework). This is essentially open. A verified handler-based AD calculus would be a real contribution.

4.2 Verified linear algebra and numerical kernels

Coquelicot and MathComp Analysis (Coq) provide foundations. Flocq (Boldo & Melquiond) formalizes IEEE 754 floating-point in Coq. Why3 + Gappa (Filliâtre, Boldo, Melquiond) handle floating-point error bounds for numerical code. HACL* verifies cryptographic primitives that include some linear algebra.

For ML: none of this is directly applied to tensor operations at scale. The closest is some verified BLAS-1-level work (vector operations), and verified small matrix multiplications. Verified GEMM at production sizes is open.

4.3 Neural network property verification (different problem)

Reluplex (Katz et al., CAV 2017), Marabou (Katz et al., CAV 2019), alpha-beta-CROWN (Wang et al., NeurIPS 2021), and the broader VNN-COMP community verify properties of trained neural networks — does the output stay within bounds for inputs within bounds, is the network robust to perturbations, etc.

This is a different problem from verifying the compiler. It's worth distinguishing: NN property verification asks "is this trained model safe?"; compiler verification asks "does the compiler produce a correct gradient/sharded program/kernel?". Both are valuable; this memo is about the latter.

4.4 Verified probabilistic programming

Tyche (some versions) and a small body of POPL/PLDI work formalize correctness of probabilistic-programming inference algorithms. This intersects memo 2 (effects, randomness) but is largely orthogonal to compiler verification.

5. Verified AD: a deeper look

This is the area with the clearest research target.

The Brunel/Mazza/Pagani approach uses linear logic to track the directionality of information flow. Forward-mode AD pushes derivatives forward; reverse-mode pushes adjoints backward. Linear negation captures the duality. The proof is by logical relations: the AD-transformed program denotes a function whose Jacobian-vector product (forward) or vector-Jacobian product (reverse) equals the mathematical derivative of the primal.

The Krawiec et al. extension handles higher-order functions by carrying a CPS transform alongside the AD transform. This lines up exactly with the Wang et al. (2019) implementation insight: reverse-mode AD is a CPS transform. The proof formalizes what Wang's implementation suggests.

Concrete next steps for verified AD:

1. Add effects. Memo 2 argued that AD over effectful programs is the open problem. Verified AD with effect handlers — proving that a with reverseMode handle e produces a program whose semantics matches the mathematical derivative of e under appropriate handlers for Random, State, etc. — is publishable.

2. Add sharding. Memo 4 argued that sharding is a refinement on the tensor type. Verified AD that propagates sharding correctly through the backward pass is a smaller but achievable target.

3. Verify a real implementation. The existing work formalizes calculi; nobody has verified a production AD implementation. A verified subset of Enzyme, Zygote, or a from-scratch system would be a real engineering effort with publishable results.

4. Bound numerical error. The above work treats AD as exact arithmetic. Real implementations use floating-point. Bounding the floating-point error of AD is open, hard, and important — gradient computation in low precision (FP8, INT4) has surprising failure modes.

6. Verified sharding: an underexploited target

Sharding propagation (memo 4) is the single most tractable verification target that nobody has worked on, and the reasoning is straightforward.

A sharded program is a program where each tensor has a sharding annotation, and operations are rewritten with collectives. The semantic claim:

For any well-typed sharded program P_sharded with mesh M, executing P_sharded on the device set described by M produces the same result (modulo numerical reordering tolerance) as executing the corresponding unsharded program P_unsharded on a single device.

This is a purely structural claim — no AD, no numerical analysis, no concurrency proof obligations. The collectives have well-defined mathematical semantics (sum, gather, broadcast). The proof reduces to:

1. Define the semantics of the typed sharding language.
2. Define the semantics of the corresponding unsharded program.
3. Show that the sharded execution simulates the unsharded execution.

The proof technique is standard simulation/refinement, the kind that has been used for distributed-system verification (TLA+, IronFleet, Verdi) for fifteen years.

Why hasn't this been done? Mostly that the sharding type systems are not formal — GSPMD's rules are documented in code, not in a paper with a proof. JAX's sharding is described in tutorials, not specifications. Step one is writing down the type system rigorously, which is itself a contribution.

This is, frankly, a six-month-to-a-year research project for someone with the right background. The deliverable: a formal type system for sharded tensors, a Coq or Lean formalization of its semantics, and a proof that well-typed sharded programs are equivalent to their unsharded counterparts. Publishable in POPL or PLDI.

7. Numerical issues: the hard subproblem

Real-number semantics and floating-point semantics differ. ML compilers happily perform transformations that are exact over real numbers but introduce floating-point error: reassociating sums (matters for f16), reordering reductions (matters for all precisions), changing accumulation precision (FP32 → FP16 accumulators).

The state of the art for verified numerics:

• Flocq (Boldo & Melquiond) gives Coq a formal IEEE 754 floating-point semantics.
• Gappa (Melquiond) discharges interval arithmetic and floating-point bounds via SMT.
• Why3 + Frama-C with the WP plugin handles floating-point contracts for C code.
• VCFloat and CoqInterval provide Coq tactics for FP reasoning.

For ML specifically: the relevant claims are not "the result is bitwise identical" but "the result is within a tolerance bound that doesn't degrade the downstream loss/accuracy." This is a probabilistic semantic equivalence in some sense, and the right framework for it is open.

The thesis I'd advance: ML compiler verification should distinguish structural claims (the right operations are performed in the right order, modulo the FP semantics of those operations) from numerical claims (the FP error is bounded). The structural claims are tractable with standard verification techniques. The numerical claims need additional work but build on existing FP verification.

8. Connection to existing systems-verification stacks

For someone with a Frama-C / eBPF-verifier / kernel-libs background, the path into ML compiler verification is shorter than it looks. The skills transfer:

• Refinement-typed C with Frama-C is the same skill as refinement-typed tensor specifications.
• An eBPF verifier is a domain-specific abstract interpreter; tensor type-checking and sharding propagation are also abstract interpretations.
• Linear-typed kernel libraries are the same skill as linear-typed tensors for AD soundness.
• A verify-core Rust crate with backend traits is the right architecture for a verified ML compiler pass: a core IR with verification annotations, multiple backends, and proof obligations discharged per backend.

The TerranoxOS Bronze proofs in Frama-C, the SigilVM eBPF verifier, the kernel-libs error-code discipline — these are not adjacent skills, they are the same skills, applied to a different IR. An "AI-native verified compilation" project is, in methodology terms, a sibling of the OS-research projects rather than a different field.

The mapping:

This is not a stretch. The verification work that has already been done on the OS projects is the prerequisite work for a verified AI-compiler project.

9. Open research problems

In rough order of tractability:

1. Formal type system for sharding. Write GSPMD's rules as a typed calculus; prove well-typedness implies semantic preservation. Already most of the way there in the Alpa and PartIR papers, but not formalized.

2. Verified sharding propagation. Build on (1): prove that the inserted collectives are correct. The hardest part is specifying the collective semantics in a way that abstracts over implementations.

3. Verified AD with effects. Extend Brunel/Mazza/Pagani to handler-based effect calculi. The Krawiec et al. CPS technique is the bridge.

4. Verified sparse code generation. TACO's correctness arguments are informal. Formalizing the level-format model and proving that generated code is correct is a real but bounded project.

5. Verified kernel fusion. Semantic preservation across fused operations is harder because of aliasing and ordering. Linear types help. Some polyhedral work has the legality conditions; lifting them to a typed setting is open.

6. Quantization with provable error bounds. Combining Flocq-style FP reasoning with quantization-specific concerns (scales, zero-points, dequant linearity). Why3 / Gappa style.

7. Verified distributed AD. Combining (2) and (3): proving that backward-pass shardings are correct given forward-pass shardings. Less clean than either piece alone but tractable.

8. End-to-end verified ML compiler. Like CompCert but for an ML language. A multi-year project; the right scope for a research group rather than a thesis.

9. Verified GPU kernels at production scale. GPUVerify-style tools work on small kernels; FlashAttention-class kernels are out of reach. This is the hard frontier.

10. Verified concurrent training. Race-free gradient updates, correct synchronization, lock-free optimizer state. Iris / Perennial-style separation logic with concurrency would be the foundation.

10. Recommendation for an AI-native language design

Concrete positions, in priority order:

• Refinement types as the primary verification surface. Users see tensor types with shape, sparsity, sharding, and effect refinements. SMT discharges most obligations. This is the right level for a production language.

• Heavyweight verification as opt-in for kernel authors. People writing FlashAttention-class code want stronger guarantees. Provide Coq/Lean/F* hooks for that subset, with the main language as the integration point.

• Verified compilation passes for the high-stakes transformations. AD, sharding, and quantization are the three where bugs are silent and harmful. Invest in proofs there; rely on testing for fusion and layout (where bugs are loud).

• Translation validation as a fallback for compiler passes that aren't fully verified yet. Better than nothing during the compiler's development phase.

• Rust-verified runtime. The runtime (memory planning, scheduling, communication primitives) should be implemented in Verus or Creusot. This is achievable today and substantively raises the reliability floor.

• A verified core IR. A small, formalized intermediate representation — something like MLIR's linalg or tensor dialect, but with a paper-and-proof companion. All compiler passes preserve well-typedness in this IR. The IR is the contract.

• Numerical claims separated from structural claims. Structural: operations in the right order, valid shardings, correct gradient structure. Numerical: error bounds, accumulation precision. Verify them with different machinery.

The thesis: ML compiler verification is about a decade behind traditional compiler verification, and the missing pieces are mostly bounded research projects that the existing methodology can solve. Verified AD over a typed core: doable. Verified sharding: doable. Verified sparse codegen: doable. Verified end-to-end pipeline: a multi-year program, achievable in pieces. The first ML compiler with a CompCert-level guarantee on its core passes will be a research milestone.

For someone whose existing work is already in this space — refinement types in C kernels, an eBPF verifier, capability-typed OS userspace — the entry cost is lower than it looks. Verified AI-native compilation is sibling to the OS research projects, not separate.

11. References

Verified compilation foundations

• Leroy, X. (2009). Formal verification of a realistic compiler. CACM. — CompCert overview.
• Leroy, X. & Blazy, S. (2008). Formal verification of a C-like memory model and its uses for verifying program transformations. JAR.
• Kumar, R. et al. (2014). CakeML: A Verified Implementation of ML. POPL 2014.
• Klein, G. et al. (2009). seL4: Formal Verification of an OS Kernel. SOSP 2009.
• Chajed, T. et al. (2019). Verifying Concurrent, Crash-Safe Systems with Perennial. SOSP 2019.

Verified AD (the core thread)

• Brunel, A., Mazza, D. & Pagani, M. (2020). Backpropagation in the Simply Typed Lambda-Calculus with Linear Negation. POPL 2020. — The reference paper for typed AD verification.
• Krawiec, F. et al. (2022). Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic Differentiation. POPL 2022.
• Smeding, T. & Vákár, M. (2024). Efficient CHAD. POPL 2024.
• Vákár, M. (2021). Reverse AD at Higher Types: Pure, Principled and Denotationally Correct. ESOP 2021.
• Wang, F. et al. (2019). Demystifying Differentiable Programming: Shift/Reset the Penultimate Backpropagator. ICFP 2019. — The CPS-AD bridge that makes the verification tractable.

Floating-point and numerical verification

• Boldo, S. & Melquiond, G. (2011). Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq. ARITH 2011.
• Boldo, S., Filliâtre, J.-C. & Melquiond, G. (2009). Combining Coq and Gappa for Certifying Floating-Point Programs. Calculemus 2009.
• Goldberg, D. (1991). What Every Computer Scientist Should Know About Floating-Point Arithmetic. ACM Computing Surveys. — Background.
• Higham, N. (2002). Accuracy and Stability of Numerical Algorithms, 2nd ed. SIAM. — The reference for numerical analysis.

SMT-augmented and refinement-typed verification

• Swamy, N. et al. (2016). Dependent Types and Multi-Monadic Effects in F*. POPL 2016.
• Filliâtre, J.-C. & Paskevich, A. (2013). Why3: Where Programs Meet Provers. ESOP 2013.
• Leino, K. R. M. (2010). Dafny: An Automatic Program Verifier for Functional Correctness. LPAR-16.
• Rondon, P., Kawaguchi, M. & Jhala, R. (2008). Liquid Types. PLDI 2008.
• Vazou, N. et al. (2014). Refinement Types for Haskell. ICFP 2014.

Rust verification (the most actively developing area)

• Lattuada, A. et al. (2023). Verus: Verifying Rust Programs Using Linear Ghost Types. OOPSLA 2023.
• Denis, X., Jourdan, J.-H. & Marché, C. (2022). Creusot: A Foundry for the Deductive Verification of Rust Programs. ICFEM 2022.
• Astrauskas, V. et al. (2019). Leveraging Rust Types for Modular Specification and Verification. OOPSLA 2019. (Prusti.)
• Ho, S. et al. (2022). Aeneas: Rust Verification by Functional Translation. ICFP 2022.

Verified cryptography (methodology reference)

• Bhargavan, K. et al. (2017). Everest: Towards a Verified, Drop-in Replacement of HTTPS. SNAPL 2017. — Project Everest overview.
• Zinzindohoué, J.-K. et al. (2017). HACL*: A Verified Modern Cryptographic Library. CCS 2017.

Translation validation

• Necula, G. (2000). Translation Validation for an Optimizing Compiler. PLDI 2000.
• Lopes, N. et al. (2021). Alive2: Bounded Translation Validation for LLVM. PLDI 2021.

Neural network property verification (related but distinct problem)

• Katz, G. et al. (2017). Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks. CAV 2017.
• Katz, G. et al. (2019). The Marabou Framework for Verification and Analysis of Deep Neural Networks. CAV 2019.
• Wang, S. et al. (2021). Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Neural Network Robustness Verification. NeurIPS 2021.

Concurrent / GPU verification

• Betts, A. et al. (2012). GPUVerify: A Verifier for GPU Kernels. OOPSLA 2012.
• Jung, R. et al. (2018). Iris from the Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic. JFP.

Probabilistic programming verification

• Atkinson, E., Sampson, A. & Carbin, M. (2024). Verifying Numerical Programs via Iterative Abstract Testing.
• Sankaranarayanan, S. et al. — various SMT-based PPL verification work.

12. Connections to the rest of the series

• Memo 1 (shapes): refinement-typed shapes are the lightweight verification at the user surface. The heavyweight verification — proving sharding inference is correct, or that AD propagates shapes correctly — sits underneath.
• Memo 2 (AD-through-effects): verified AD over a typed effect calculus is the most concrete research target in this series. Brunel/Mazza/Pagani plus algebraic effects equals a publishable POPL paper.
• Memo 3 (sparsity): verified sparse code generation extends TACO with formal proofs of correctness. Particularly important because sparse code is bug-prone.
• Memo 4 (distribution): verified sharding propagation is the underexploited tractable target. A purely structural simulation proof; the type system does most of the work.
• Memo 6 (hardware abstraction): verified lowering to hardware-specific kernels — proving that a high-level operation correctly compiles to a tiled, vectorized kernel — is the hardest verification target and the main subject of memo 6's discussion of correctness.

13. Cross-memo synthesis update

The unified-type-system thesis from memos 1–4 ("tensor type with four refinement axes: shape, effects, structure, sharding") gains a fifth axis here: proof obligations. Each refinement axis carries verifiable claims, and the language can stratify them by verification weight. Lightweight refinements (SMT-discharged) for the surface; heavyweight refinements (proof-assistant-discharged) for the kernel-author tier; translation validation for the compiler internals during development.

The framework is starting to look less like "a research language" and more like "a verified-compilation pipeline with a refinement-typed surface language as its frontend." The memos have been converging on a multi-tier architecture without explicitly designing for it.

14. Next memo

Design Space 06: Hardware Abstraction. The final memo. Modern AI hardware is a zoo: NVIDIA GPUs (multiple generations with incompatible features), AMD GPUs, TPUs, Cerebras wafers, Graphcore IPUs, dataflow architectures (Tenstorrent, Groq), and CPUs with ML extensions. Each has its own cost model, memory hierarchy, and concurrency model. The question: what is the right level of hardware abstraction for an AI-native language? Triton's tile-level model? MLIR's dialect-per-target model? CUDA-style explicit hierarchy? And how does this compose with the previous five memos' refinement-typed tensor model?