Sent from my iPad > On Mar 29, 2020, at 2:46 PM, Luke Kenneth Casson Leighton <lkcl at lkcl.net> wrote: > > also if you can work out how the formal proofs work, and how to extract the > links into the BSV code or plug in the nmigen library, that would be really > handy. Currently, BSV uses the SMT Yices solver.