We're excited to announce the new Certora AI Composer, an open-source AI coding platform that composes artificial intelligence with formal verification to make smart contract development faster and safer.

Unlike generic “AI-for-code” tools that focus on speed and convenience, Certora AI Composer ensures that every AI-generated snippet adheres to mathematical safety rules before it ever runs. By embedding Certora’s proven formal verification technology directly into the AI generation loop, developers can explore design ideas confidently while knowing that security invariants are continuously checked rather than retrofitted.

“Using AI should never mean compromising safety. Certora AI Composer proves that AI and formal verification can work together to make smart contract development trustworthy by default,” Certora Founder Mooly Sagiv explained. “This alpha release is our invitation to the community to help us shape the future of safe autonomous coding.”

The Certora AI Composer Alpha will be open source starting Dec. 4 and will be available to the community on GitHub. Developers are encouraged to experiment, provide feedback, and contribute to shaping a new standard for verified AI-driven development.

Key Features:

• Integrated formal verification checks for AI-generated code
• Open-source extensibility to build your own safety modules
• Backed by the Certora Prover, Certora’s industry-trusted verification engine

We will also be hosting a livestream event on Dec. 4 titled “AI Meets Verification: An Open Discussion with Certora Researchers,” which will provide a detailed description of how Certora AI Composer operates and what it can do to enhance security. 

Be sure to sign up for the event HERE. 

And remember to follow us on Twitter at @CertoraInc for future updates and reminders.