11:42 <catlosgay[m]> ic3 is the state of the art in model checking and way stronger than k-induction (particularly smtbmc's implementation)

11:42 <catlosgay[m]> ric3 is bit level so will struggle a bit with memories that have to be bit blasted, but otherwise its very good and not far from performance of the commercial tools on many problems

11:46 <catlosgay[m]> > today i'm broadly disinclined to do anything with a technique whose loudest advocate and the person who wrote the most documentation on it is an outspoken transphobe who i will ban on sight anywhere i have the power to do so

11:46 <catlosgay[m]> totally agreed and it would be nice to build up some better materials separate from him. if you have any designs lying around you think might be interesting to formally verify I am planning to do some more verification soonish and can probably write some of that up as case studies. an annoying thing working on the model checking algorithms side is that we don't actually have particularly good collections of properties to see what

11:46 <catlosgay[m]> people actually write/the techniques they use to get proof convergence - particularly not from those that have training in industry rather than guessing at things in open source - so I have been thinking maybe I should just go through and verify some designs for this

12:13 <anuejn> oh that sounds lovely

14:46 <Stas[m]1> having small, even tiny formally verified stream modules can lead to robust building blocks for complex things

14:46 <Stas[m]1> things like repeaters, packetizers, header adders