Introducing the Verified Code Translation Research Awards

Today we’re launching the Verified Code Translation Research Awards, a new award program supporting university faculty whose research advances the scientific foundations of verified code translation.

Verified translation depends on foundational research in defining formal semantics, designing techniques for verifying program equivalence, and building open-source tools that are improved and maintained by a strong formal methods community. Just as the internet created shared infrastructure that others could build on, we need to invest in the foundations of verified software so researchers and companies can build practical systems on top of them.

At Code Metal, we advance AI and formal methods to make high-assurance software possible for work of consequence. That work stands on decades of academic research, and this program is our way of investing back into the community pushing those foundations forward.

What we’re funding

From August 18th to October 8th, we will be accepting proposals for research that explores the use of formal methods and/or AI to advance verified code translation.

We’re interested in the underlying science that can make translation trustworthy: demonstrating that programs preserve their behavior across different languages, formalizing the semantics of the languages and systems involved, and developing reusable methods and tools that others can build on.

Our panel of expert judges will select up to four proposals for outstanding merit and relevance to the call for proposals, with the winners receiving awards ranging from $10,000 to $40,000, paid to the awardee’s host university as an unrestricted gift. Larger awards may become available in future phases, based on outcomes from this first round.

Beyond funding, winners will also be invited to present their work through Code Metal’s research programming, including our Formally Speaking seminar series and future academic convenings, and will be featured on the Code Metal research website.

Awardees retain ownership of all work products developed under the award, and we encourage recipients to openly publish their findings and make their code open source.

Research areas of interest

We welcome proposals across formal methods and AI, with particular interest in approaches that can handle equivalence across multiple programming languages. Priority areas include:

Verified code translation: techniques demonstrating that translated code preserves the behavior of the original program across languages, platforms, and hardware targets, particularly for C, C++, Rust, CUDA, OpenCL, VHDL, MLIR, Python, and Octave.
AI-assisted verification and validation artifacts: systems that use AI to produce contracts, test harnesses, lemmas, proof sketches, type refinement maps, translation certificates, or other evidence checkable by independent tools.
Analysis tools for industrial programming languages: scalable static and hybrid analysis tools for Python, C, C++, Rust, and other industrial languages, including analyses for types, dependencies, values, shapes, effects, and program behavior that enable trustworthy translation, verification, testing, and code generation.
Formal semantics of programming languages: mechanized proofs of cross-language semantic equivalence, executable specifications, and mechanized models for programming languages, intermediate representations, and hardware programming models.
Trustworthy optimization and hardware targeting: verified optimization, accelerator targeting, compiler correctness, semantics-preserving lowering, numerical correctness, and hardware-aware code generation.
Specification-aligned code generation: combining language models with types, refinement types, program logics, symbolic reasoning, theorem proving, contracts, or independently checkable proof obligations.

These topic areas aren’t exhaustive, and if your work advances verified translation, we want to hear about it.

Who can apply

The program is open to faculty members at accredited universities. Research groups may apply jointly, provided one named Principal Investigator accepts responsibility for the project. Full eligibility requirements are available in the full terms and conditions.

Proposal requirements

A complete proposal consists of:

A project summary (max 3 pages) covering your research agenda, technical approach, timeline with milestones, expected deliverables, and how the work advances verified translation
A budget overview (max 1 page), with overhead and indirect costs capped at 10% of the total award
One-page CVs for the PI and significant contributors, with links to DBLP and/or Google Scholar
Organizational details (timeline and expected outcomes) and a brief conflict-of-interest disclosure

Timeline

Submissions Opening Date: August 18, 2026
Submission Deadline: October 8, 2026
Awards Announced: December 8, 2026

How to apply

Submit your proposal at this link by October 8, 2026. Full program details, eligibility requirements, and terms are available on the full terms and conditions page.

We’re excited to help promising ideas in verified translation grow into the tools and techniques that mission-critical software will depend on.