Automating formal verification of safety and security prop-erties in both hardware and software systems is challengingdue to a number of issues. In this paper, we tried to addresstwo important challenges in this regard. The first challengethat we discuss is the scalable co-verification of hardwareand firmware in a modern system-on-chip (SoC) platformto guarantee end-to-end security of the system. We havediscussed two specific problems in this regard that we havetried to solve and our approach to address this challenge, (i) we designed a verification methodology for end-to-end secu-rity property verification for authenticated firmware loaderprotocol running on a SoC platform, and (ii) we proposeda unified framework called HyperFuzzing, for specifyinghardware security properties and automatically testing forviolations of these properties using fuzzing. The second chal-lenge we have discussed in this paper is to verify hardwareor software systems that use closed-box functions or opera-tions. To address this challenge, we have introduced a newtheory for SMT solvers, called closed-box function theory,and have implemented it in our prototype solver Sādhak. Our solver Sādhak can handle SMT constraints with closed-box functions, which can be used by verification and testingtools for solving closed-box constraints.