Technical interest · T-02
Formal verification
Proving that code meets its specification, and using LLMs to write the specifications in the first place.
In the AI Safety & Agent Harness fellowship I built an LLM-driven system that synthesizes specifications for C and Rust code and checks them with Frama-C/WP, Alt-Ergo and Lean 4, using mutation testing to reject specifications too weak to mean anything.
Nearest neighbors · any layercosine distance in the full space