I hate to be the one to break it to you, but you did not invent the idea of reducing the good behavior of programs to first-order logic properties and to apply

I hate to be the one to break it to you, but you did not invent the idea of reducing the good behavior of programs to first-order logic properties and to apply an SMT solver to these. You are not even at the point where you might compare your false-positive rate to their false-positive rate, but if someone was going to change the future with that idea, the future of 20 years ago would have been changed. And perhaps it was. But if SPARK83, to take one system amongst others, did not prevent Heartbleed, I don't see how your system “can prevent Heartbleed”. It can't, because Heartbleed is not written in the language at https://github.com/tomprimozic/type-systems/blob/master/refined_types/expr.ml#L75 https://github.com/tomprimozic/type-systems/blob/master/refi... Describing your github repository with the words “can prevent Heartbleed” is disingenuous and unscientific. You should keep the dramatic hyperbole for the grant proposals.