Comment by leni536

Can proof assistants help (like coq)? My best bet is the specification of crypto algorithms are essentially the algorithm themselves, so maybe not. Of course if you want to avoid state than maybe you want to program your crypto in a functional language, although there could be non-trivial attack vectors too (like timing).