Verified branch relaxing assembler in Isabelle/HOL with provably minimal bytecode layouts
No issues yet.