AI Safety & Agent Harness Research Fellow

LLM-driven specification synthesis that turns C and Rust code into machine-checked proofs in Frama-C and Lean 4.

• Built an LLM-driven specification synthesis system spanning C/ACSL and Rust/Lean 4, integrating Frama-C/WP, Alt-Ergo, Charon/Aeneas, mutation-guided refinement, executable counterexamples, and kernel-checked proofs.
• Achieved a 0.976 mean mutation kill rate versus a 0.622 baseline across 189 Lean benchmarks while reducing prover calls 11-fold (19.9 vs. 224.8) and wall time 2.4-fold (71 vs. 168 seconds) with a five-gate validation oracle.
• Closed an end-to-end verification chain on the production Rust crate gcd 2.3.0: proved 11/11 specifications with 0 refuted and generated a 40-theorem, zero-sorry Lean proof comprising 8 soundness goals and 32 supporting lemmas.
• Delivered 10 certified C artifacts with Frama-C/WP and Alt-Ergo, discharging up to 27/27 proof obligations; imported 35 benchmark algorithms and rejected weak specifications through property-based and TCE-filtered mutation testing.