Using a bounded model checker to provide absolute guarantees on runtime behavior. Signed-off-by: Zachery Aaron Shores-Chmielewski <zacheryasc@gmail.com>