In safety-critical domains, extensive software testing is required to validate functional properties and meet standards such as ISO-26262 and DO-178C, which mandate strict code coverage levels. Uncovered code sections may indicate insufficient testing or unreachable code, leaving latent defects undetected.

Traditional coverage tools reveal such gaps but cannot determine their cause. Fuzzing effectively discovers bugs but cannot prove unreachability, while bounded model checking (BMC) can formally prove unreachability and generate test cases but inherently underapproximates program behavior due to bounded exploration.

We present a hybrid testing framework that combines fuzzing and BMC in a concurrent, automated workflow. It measures baseline coverage, instruments uncovered regions, and applies both techniques to either generate additional inputs or prove unreachability. The resulting tests and proofs help identify untested requirements, requirement violations, and dead code. Applied to a subset of an industrial-grade C standard library for embedded automotive systems, our approach achieves more efficient coverage than standalone fuzzing or BMC, while also identifying unreachable code and specific decision constellations, demonstrating its potential for broader adoption in safety-critical domains.