Code Integrity
Rooted in Certainty

The primary reason we don't already have more software security is the labor bottleneck. Formal methods code is usually written by PhD-level engineers, and usually requires 10×—100× as many lines of code as what's being verified. As frontier AI labs make progress on reasoning, the labor bottleneck disappears.

Without software verification, the transition to AI-driven software development may pose severe risks:

• Code is not adversarially robust. Coding AIs may increase volume and velocity of attacks on software infrastructure.
• LLMs are not adversarially robust, and cannot be deployed as complete stand-ins for review, testing, and bug-finding.
• As we deploy superhuman models without fully understanding their generalization behavior, we need methods for supervising AIs without understanding the full implementation of their solutions.

At Theorama, we're building the infrastructure to make this possible.

We're generating domain-specific synthetic datasets with verification-specific advantages:

Iterative Denoising to Leverage Error Messages

Proof assistant error messages have rich structure. We start with a correct proof, add various errors or make omissions, then record a trace of fixing the issue. This transforms an RL problem into an SFT problem.

Planning via Autoinformalization

Theorems may have multiple different proofs, from different abstractions, different languages, or different versions of the proof software. Autoinformalization augments the dataset and provides fine-grained information about engineering choices.

These approaches allow us to train models specifically tailored to verification tasks.

We're measuring and improving domain-specific reasoning for verification. Frontier models augmented with RAG and in-context examples can solve small verification tasks. The major challenge is developing scaffolding that leverages these boosts systematically.

Transpilation

We're quite excited about translating CompCert from Coq to Lean, which will serve as a demonstration that models can handle industry-scale verification projects.

Following Reasoning Templates

The next step is to gear at projects like CompCert but for Rust, where a large fraction of the reasoning is within domain, and we have significant data and infrastructure for the required creativity for the harder parts.

This approach allows us to tackle increasingly complex verification tasks with scalable approaches.