This paper summarises our experience in using model checking technology to understand concurrent programs. We use Verisoft to understand various aspects of a rewall tool kit. We instrument three components of the rewall tool kit with Verisoft hooks in order to test their behaviour. Some of the key changes include changing socket communication to message passing queues and adding appropriate synchronisations so that the behaviour of the system can be tracked. We aim to minimise the number of changes to the original source code so as to not a affect its real behaviour. The main conclusion is that it is possible to inspect source code with a view towards verifying key behavioural properties.