The formal css proof is here. It's a gzip'd tar file of Lego source code.
This is a mathematical proof that an abstract mathematical relation known as CSS has an output for every input.
This is entirely abstract mathematics — no mention of computers, programs, or computability, in sight.
But inevitably — due to the Curry-Howard isomorphism — our proof contains a program implementing CSS.
The theorem prover I used to write the proof - Lego - can directly interpret the proof as a program, although very inefficiently.
Possession of such a program is illegal in the US & maybe elsewhere? Does that make this proof illegal too?