Bridging Requirements and Assurance: Neurosymbolic Autoformalization for C++ Verification and Requirements-Coverage Testing (Keynote)

We describe a neurosymbolic approach for the autoformalization of natural-language requirements into machine-checkable specifications. Our approach combines neural language models with symbolic reasoning to translate informal requirements into a structured executable representation amenable to downstream symbolic execution. This formalization serves as the foundation for two complementary assurance activities: (1) verification and automated test case generation for C++ implementations, ensuring behavioral conformance to specified requirements; and (2) requirements-coverage-driven test generation, producing test suites that achieve traceability and coverage criteria demanded by certification standards. The approach provides an integrated path from specification to certified assurance, reducing manual formalization effort while improving consistency between verification artifacts and certification evidence.