Shower idea

Implement a web browser using a language that supports dependant types in order to prove its correctness and that no vulnerabilities exist for it.

depndent types don't prove that no vulnerabilities exist. correctnes proofs do that but only for the part covered by the specification, so it still makes it possible to have bugs you didn't think of while designing a proof.