Traditional software testing aims to find errors by running systems through numerous scenarios. In contrast, formal methods use rigorous mathematical techniques to prove that software or hardware behaves as specified across all permitted inputs and states, thereby proving the absence of entire classes of errors. This distinction is becoming increasingly critical as AI accelerates code generation, making systems too complex and consequential to rely solely on testing for security.
Recent cyber incidents highlight the stakes. Earlier this month, ASOS investigated unauthorised activity after its app sent threatening notifications, potentially exposing personal information. Last week, critical flaws in PHP prompted global website shutdowns for emergency patching, with exploitation attempts already reported. While formal methods wouldn't prevent all breaches like social engineering, they could establish a stronger foundation for critical components, providing mathematically verifiable evidence of correct behaviour.
ARIA's Safeguarded AI programme is investigating the practicality of AI-enabled formal methods for modern digital infrastructure. The eight new research projects, each receiving backing, aim to test AI's ability to produce proofs for production-grade software and hardware affordably and quickly, enabling wider use beyond specialist systems. Projects will be built by Blue Teams and independently tested by a Red Team for weaknesses.
The projects, which began on 1 September and operate in eight-week sprints, cover diverse areas. These include extending hardware security architectures like CHERI to protect AI models on chips, formally verifying compiler infrastructure like LLVM, building secure agent sandboxes on verified operating system kernels like seL4, and developing verifiable browsing solutions for sensitive networks. Other projects focus on creating high-performance AI inference stacks with formal proofs, verifying Android's pKVM for on-device AI, and building network guards for industrial control systems with AI-generated specifications.
Trail of Bits acts as the independent Red Team, testing the security claims of the Blue Teams by examining specifications, verification tools, and threat models. Their role is to sharpen assurance cases and build trustworthy software.
Early results indicate significant speed improvements, with AI systems handling substantial engineering and proof work under human oversight, potentially reducing tasks that once took months to days. This suggests formal guarantees could become a realistic expectation for critical software. While AI accelerates proof generation, defining the correct security properties still requires extensive expert judgement and adversarial scrutiny. Teams are also addressing the challenge of keeping proofs current as systems evolve.
