Formally Verified Software Synthesis
Utilize formal verification techniques to synthesize software that is provably secure, reducing vulnerabilities and enhancing system robustness. Traditional programs in these areas have tended to assume that AI capabilities are saturating, leaving important avenues neglected.
Efforts could break down into several key components:
• Specification generation and validation tools
• Code and proof generation systems
• Tools that integrate formal verification into existing engineering workflows
• Practical formalization structures that facilitate real-world adoption
Resources (16)
ARIA Opportunity Space: Safeguarded AI
Funding Program
DARPA Program: ARCOS - Automated Rapid Certification Of Software
Funding Program
DARPA Program: HACMS - High Assurance Cyber Military Systems
Funding Program
DARPA Program: TRACTOR - Translating All C to Rust
Funding Program
Project Everest
Initiative
The seL4® Microkernel
Initiative
Formally Verifying WebAssembly - A Soroban Case Study
Whitepapers and Essays
Provably safe systems: the only path to controllable AGI
Whitepapers and Essays
Towards Guaranteed Safe AI: A Framework for Ensuring Robust and Reliable AI Systems
Whitepapers and Essays
Galois
Company
Jason Gross’s PBC
Company
Atlas Computing
Research Org
Beneficial AI Foundation
Research Org