I have implemented and contributed to automated reasoning systems in my preferred language OCaml. Both efficiency in dealing with large logic formulas and interfacing with other solvers have been recurring themes here.

Simulink Design Verifier

I am working as a developer on the Simulink Design Verifier that can verify that your Simulink model corresponds to stated requirements, and is free from certain errors without generating actual code.

Kind 2

The Kind 2 model checker takes a Lustre program as input and tries to automatically verify given safety properties with k-induction and a variety of additional techniques. It uses the SMT solvers Yices, Z3 or CVC3 and can run in a parallel mode, supported by incremental invariant generation.


The iProver-Eq system is an automated first-order theorem prover based on the successful iProver system. It implements an instantiation-based calculus modulo equality and delegates ground reasoning to an SMT solver, currently supporting CVC3, CVC4 and Z3.


You can find the following side projects developed in other contexts on my Github page.

  • cvc4-ocaml: An OCaml interface to the CVC4 SMT solver, currently only supporting the QF_UF theory.
  • ocamlczmq: An OCaml interface to the ZeroMQ library, using the CZMQ library as an abstraction layer
  • smtlib-mode: An Emacs mode to edit SMTLIB2 files

Picture of me

Dr. Christoph Sticksel

Senior Team Leader and Principal Software Engineer in
Formal Methods/Program Analysis at
Natick, MA