[kzrdude]

I guess it was done as an afterthought? This is supposed to be a lean formalization https://github.com/openai/cdc-lean