[aseipp]

Why not picorv32? Size-optimized, open licensed (no 64-bit, but that's where you could come in and be a star!) Clifford Wolf, the author, also wrote Yosys and Icestorm, which you can use to synthesize picorv32 for the iCE40 FPGAs with a fully open source HDL toolchain. It's really nice and usable!

Clifford has also been doing a lot of cool work adding SMT-based verification tech for synthesis via Yosys, and even started working on a verification bench for RISC-V implementations: https://github.com/cliffordwolf/riscv-formal - he's also very nice and approachable IMO. I'm sure he'd appreciate some extra help.

Sounds like exactly what you want, perhaps.