Natalia Klaus is a verification engineer at Runtime Verification, where she works on formal verification of Linux kernel code in Rust and C. She builds the Rust-to-Lean 4 pipeline (Charon, Aeneas) and uses AI provers to close proof obligations within the Ethereum Foundation's zkEVM Verification Project, with verified targets including Plonky3 FRI folding and RISC Zero Merkle inclusion. Previously she verified the Tezos OCaml codebase at Formal Land. She holds a Master's degree in Systems Analysis from Southern Federal University, with a focus on lambda calculus, mathematical logic and category theory.