A clear-eyed technical assessment of formal verification for AI-generated code: which approaches are credible, what barriers remain, and where the market will emerge first.

What Automated Transpilation Actually Costs, and What It Doesn't

How Code Metal combines AI with formal methods to build trusted code translation systems, and welcoming Prof. Loris D'Antoni as our first Code Metal Scholar.

Introduces gpuFLOPBench, a benchmark containing 577 CUDA kernels to evaluate whether language models can predict floating-point operation counts without execution, revealing limitations in understanding hardware-specific performance details.

LLMLift uses large language models (LLMs) to automate code translation between domain-specific languages (DSLs), ensuring functional correctness and outperforming traditional tools in speed and efficiency.

Compares structured workflows versus agentic approaches for MATLAB-to-HDL translation, showing that agentic methods with the Model Context Protocol increase simulation reach rates by over 20 percentage points on mid-sized models.

Introduces UniPar, an evaluation framework for assessing how large language models translate between parallel programming languages, achieving 69% compilation success and 33% functional correctness through fine-tuning and compiler-guided repair.

MONOCODER is a smaller, HPC-specific language model that outperforms larger, general-purpose LLMs on HPC code tasks, offering better performance in code generation and comprehension.

Advanced techniques for deploying and optimizing large language models on resource-constrained edge devices without compromising performance.

Domain-specific languages (DSL) have been a common alternative to general-purpose programming languages to implement domain-specific optimizations and simplify programming of domain-specific hardware