With increasing capabilities of AI models to perform cybersecurity attacks, eliminiating code-level vulnerabilities becomes an essential requirement for critical embedded software, in particular in the defense domain. Static analysis by abstract interpretation can prove the absence of vulnerabilities due to runtime errors, e.g., buffer overflows, and flow-related vulnerabilites such as command-injection. We'll present the methodology and report practical experience with the Astrée analyzer.