Professor Hunt's research involves the use of formal mathematics to write specifications for computer hardware and software and to use proof techniques to determine the validity of such specifications. Specifications of both high-level intent and low-level implementations are possible, and mechanical proof techniques can determine whether implementations satisfy their specifications. Over the years, he has verified a number of different microprocessor designs of increasing complexity. Professor Hunt is also working actively in the area of RSFQ-based circuits; these very-low-power circuits must be cooled to 4K to operate correctly. He is also interested in computer architecture, low-power computing, garbage collection, and parallel computing. Currently, he is working to parallelize several theorem-proving algorithms.