Romanian-American computer scientist, professor at UC Berkeley.

Invented proof-carrying code (1997): a paradigm where programs carry machine-checkable proofs of their own safety properties.

The consumer verifies the proof before execution — no trust in the producer required, only trust in the proof checker.

This is the ancestor of verifiable computation in cyber: every state transition carries a STARK proof that the verifier checks without re-executing the computation.

Proof-carrying code shifted the burden from runtime monitoring to compile-time verification, influencing type systems, certified compilers, and formal methods.

His insight that proofs are cheaper to verify than to produce is the economic principle behind proof-of-useful-work in cyber.

Local Graph