Mathematical proof, grounded in real code.
Making AI useful for hard engineering problems
Performance without sacrificing correctness
Our ideas are grounded in real engineering problems, real codebases, and systems where correctness, performance, and trust matter. We move beyond theory by applying research where the consequences of software failure are real.
We contribute to the research community by sharing findings, benchmarks, technical reports, and open-source tools that advance the state of the field. Our researchers publish, present, and collaborate across papers, conferences, seminars, and academic partnerships.
We bring together researchers, engineers, and domain experts across AI, programming languages, systems, and formal methods to challenge assumptions and advance what high-assurance software can become.
featured
What it takes for a type mapping between a source and target language to be correct — conversion soundness and round-trip preservation — and how Code Metal uses schema-based interface generators to build verified, behavior-preserving type mappings.
read on
The University of UtahTyping Python, Gradually
UtahTranslation Validation for LLVM's AArch64 and RISC-V Backends
MITScaling Formal Verification to Complete Hardware-Software Stacks
Browse the full series
view all
We're hiring researchers, engineers, and builders to bring trustworthy AI to systems that can't fail
open roles
