Certora compares fuzzing vs formal verification on Soroban, showing Sunbeam finds exact counterexamples fuzzing misses.

Exact wrong-key distributions for PRESENT-like SPNs, and yes, the randomization hypothesis is formally false.

Paper on SMT encodings for quantum circuit optimization, with exact-G and null-gate variants that synthesize S-box circuits faster than e...