Good morning all, creator here- I made this demo for you to explore a requirements engineering technique. Defects in the requirements engineering process have o

Good morning all, creator here- I made this demo for you to explore a requirements engineering technique. Defects in the requirements engineering process have outsized cost in the overall product development cycle, especially in safety critical applications. Adding just a dash of formal methods in authoring tools can catch defects as they are introduced and provide timely feedback to engineers. This is a quick example of how to use a context-free grammar and an SMT solver (Z3 in this case) to automatically find logical contradictions, redundant conditions and inconsistency of entity names. Enjoy!