Cosmin Rădoi
Writing here about AI safety, timelines, and verification.
Co-founder, CEO and CTO of Asymptotic. AI agents will soon write all the world’s code, but having them review their own work leaves dangerous gaps. The only correctness guarantees that scale are machine-checked mathematical proofs. Asymptotic builds the infrastructure and agents that prove both code and agent actions correct. Beachhead: formal verification of smart contracts in the Sui ecosystem. More languages and ecosystems soon.
Founded Unhack in 2017 and designed the language for large-scale code transformation now known as GritQL, open source and used in Biome. The company raised a $7M seed led by Founders Fund and Abstract and was renamed Grit. Left in 2023, Grit was acquired by Honeycomb in 2025.
PhD in Computer Science from the University of Illinois at Urbana-Champaign, on program transformation and rewriting, advised by Grigore Roșu. Core developer of the K Framework; led its Java reimplementation. Two ACM SIGSOFT Distinguished Paper Awards (ISSTA 2013, ICSE 2015).