We introduce a simple dynamical system that describes key features of a bilateral nuclear arms
control regime. The evolution of each party's beliefs and declarations under the regime are represented, and
the e ects of inspection processes are captured. Bounded analysis of this model allows us to explore { within
a nite horizon { the consequences of changes to the rules of the arms control process and to the strategies
of each party, bounded scope invariants for variables of interest, and dynamics for initial states containing
strict uncertainty. Together these would potentially enable a decision support system to consider cases
of interest irrespective of unknowns. We realize such abilities by building a Python package that draws
on the capabilities of a Satis ability Modulo Theory (SMT) solver to explore particular scenarios and to
optimize measures of interest { such as the belief of one nation in the statements made by another, or
the timing of an unscheduled inspection such that it has maximum value. We show that these capabilities
can in principle support the design or assessment of future bilateral arms control instruments by applying
them to a set of representative and relevant test scenarios with realistic nite horizons.