We love formal methods

We specify, model and verify code and designs using formal logic.

Properties can be anything you can specify in logic. It can range over a function, or an entire program.

We check those properties against concrete inputs (runtime verification) and symbolic inputs (formal verification), and explore all possible behaviors of the code, to give you the highest possible assurance.

Our approach is based on the  K Semantic Framework.