Cezar-Constantin Andrici

I am a Ph.D. student at MPI-SP, Germany, until December 2026, working with Cătălin Hriţcu on securing verified F* programs against linked unverified code. Currently, I am also a research intern at Microsoft Research in Cambridge, UK, working with Son Ho on verification tools and proof automation for Rust programs.

Email: cezar.andrici@mpi-sp.org

Motivation

My goal is to bring trust to digital systems. More of our lives run on software every day: our money, our identities, our public services, our votes, and soon the autonomous robots around us. We are asked to trust this software, and the companies and institutions behind it, with our data and our safety, yet we have little evidence that it deserves that trust. As a growing share of code is written by AI, faster than anyone can review it, this gap only widens.

Law and policy try to restore that trust, but compliance often turns into a formality that people neither understand nor believe protects them. Audits and testing help, but they struggle to keep up and cannot offer mathematical guarantees. Formal verification can: a machine-checked proof holds no matter who, or what, wrote the code. My research works toward making such guarantees practical for real programs: verifying effectful code in proof-oriented languages such as F*, and securely compiling verified code so that its guarantees survive when linked with unverified code. I use AI agents every day to write both code and proofs, and I believe they will make verification cheap enough for all critical software.

Research Projects

Verification of Rust programs with Aeneas

I am extending Aeneas to verify Rust programs that manipulate raw pointers directly. Aeneas translates safe Rust into pure functional code, which keeps proofs simple, but this approach does not apply once a program uses raw pointers in unsafe code. To handle such programs, I am adding support for separation logic to Aeneas, targeting its Lean backend, together with proof automation so that these proofs stay as simple as possible.

Secure compilation from F*

My Ph.D. thesis is about securely compiling programs verified in F*, a proof-oriented programming language: the guarantees proved in F* should still hold once the compiled code is linked with unverified code. I developed SCIO* for programs with IO (POPL 2024) and SecRef* for programs that share mutable references with unverified code (ICFP 2025). Most recently, I developed SEIO*, which securely extracts F* programs with IO to an OCaml-like language (ICFP 2026).

Verified SAT solving in Dafny

Earlier, I built TrueSAT, a verified implementation of the DPLL algorithm, the basis of modern SAT solvers, in Dafny, a verification-aware programming language (FROM 2019, Mathematics 2022).

News