In this paper we discuss the application of a range of techniques to the verification of mission critical ﬂight software for a JPL mission. It is clear that for this type of application we want to achieve a higher level of conﬁdence than can be achieved through standard software testing. Unfortunately, given the current state of the art, especially if one has to comply with the tight deadlines and resource limitations of a ﬂight project, it is not feasible to produce a rigorous formal proof of correctness of a ﬂight ﬁle system. This means that we must look for a practical alternative in the gray area between traditional testing and proof, trying to optimize rigor and coverage as much as possible. The approach that we describe here is based on a combination of random testing, model checking, and static source code analysis. The results we have obtained are encouraging, and suggest that for more complex properties of programs with complex data structures, it is possibly more beneficial to use constraint solvers to guide execution (i.e., testing, even if performed by a model checking tool) than to translate the program and property into a set of constraints, as in abstraction-based and bounded model checkers.