Automating Formal Proofs for Reactive Systems

Hoping to read in detail later, but very interesting at first glance thanks!<p>Have thought for awhile that many systems would benefit from one or more &quot;guard&quot; components for which we have formal proofs that no bad things can happen - e.g. you write an equity trading application in Python, but route all the trades through a checker that ensures you aren&#x27;t trading too much or too often [1].<p>[1] See Knight Capital 2012, <a href="http://en.wikipedia.org/wiki/Knight_Capital_Group#2012_stock_trading_disruption" rel="nofollow">http:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Knight_Capital_Group#2012_stock...</a>

So one builds a model in Reflex based on the requirements, then tests that model. Even when the requirements are complete (which often they are not), the real life implementation afterwards may still bring zillions of problems (my own bugs, using a bad framework, whatever) which this model testing cannot catch... eh.

Interesting approach, I can see this being of great use, I will definitely take a closer look. also, nice video- especially the soccer references.