Why verified software remains elusive

Machine checkers for software have been getting steadily stronger for decades; we now have fully verified compilers (CompCert) and even OS kernels (seL4). Yet software verification continues to have low uptake. If checker strength were the bottleneck, adoption should have followed. So why hasn't it?

The trust-building verification loop#

To answer this question, verification must be seen as a process loop that builds trust in the software over time:

1. Specification: deciding and communicating what to prove.
2. Verification: scalably performing the proof.
3. Proof reporting and maintenance: exposing proof results to the user and maintaining them.

Most of the advances in verification to date have been concentrated on developing novel proof languages and scalable verification algorithms; these are tools that live on the verification side. The core bottleneck to adoption is interfacing these tools with developers in the wild. This interface is where the rubber hits the road.

Specification: deciding and communicating what to prove#

While developers usually have specifications or invariants in their heads, traditionally verification has required exporting specifications into formal languages. First, this is challenging for the majority of developers due to unfamiliarity with formal languages. Second, formal specification languages just aren't very interpretable, making formal specifications a poor way of communicating claims and intents between developer teams. This is why the spec either never gets written or quietly rots after the first refactor. Specification, in practice, is an authoring problem long before it is a math problem.

At Aretta we recognized this problem early and built our SDK Aristo to remove it. Aristo puts the claim in the code, in plain English, directly above the function it describes:

#[aristo::assume("lo <= hi")]
#[aristo::intent("returns a value within [lo, hi] for any input", verify = "neural", id = "clamp_in_range")]
pub fn clamp(value: i64, lo: i64, hi: i64) -> i64 {
    value.max(lo).min(hi)
}

The assumption records the precondition the function relies on (an interval only makes sense when lo <= hi), and the intent records what the function guarantees under that assumption. The verify field selects how rigorously the claim is checked, from a fast local AI critic (neural) up to machine-checked proof (full). Together they address both halves of the problem: authoring needs no formal language, just plain sentences any engineer can write, and the claims are visible to every teammate and every tool, in the diff, next to the code they describe.

Agent-enabled: Because Aristo ships as agent skills, it works out of the box with coding agents like Claude Code. Your agent writes these annotations as it works, and you only attest to them. Attesting is simple: the skill proposes the claim, and you as the developer accept or reject it, since the final agreement on what the code should do has to involve the developer.

Verification: performing the proof#

Once a claim exists, checking it has to run against the real codebase, and the obstacle there is observability. The state a property talks about (e.g., a private counter inside a cache, or a flag inside a write-ahead log) is deliberately hidden behind the API, and rightly so. Encapsulation is good engineering, but it also means a checker cannot see the state it needs to inspect. Aristo provides observability hooks that expose exactly this state without changing the API you ship: derive-style snapshots that let a harness read private state directly. Beyond observability, Aristo also provides test-only visibility for crate-private functions and labeled fault points for exercising failure paths. All of these hooks are feature-gated, so they compile away entirely in production builds.

#[derive(Inspect)]          // feature-gated: compiles away in production builds
pub struct Cache {
    #[inspect]
    evictable: usize,       // gains inspect_evictable()
    // ...
}

The proving itself runs on Aretta's backend. The same claim can be checked today by a free local critic, then escalated to tests, fuzzing, and machine-checked proof, which is the full service we run with design partners. To make it concrete, here is one guarantee we check for Turso, a production database engine, verbatim:

The cache's materialized evictable-page counter stays equal to the true number of evictable resident pages after every cache operation.

That counter is private state inside the cache, and the guarantee is checkable against the running engine only because the observation points exist. No fields were made public and no fork was needed.

Reporting and maintenance: keeping the proof alive#

The last leg of the loop is the one most verification efforts never build, and it comes down to two abilities: communicating what was proved in terms the developer already speaks, and re-running the proof whenever the code changes.

Aristo handles the first by keeping every claim's status with the code. A claim reads as a plain sentence, its verdict is stored alongside the function, and there is no formal report to decode. It handles the second by hashing each claim against the function body, so that editing verified code flips the claim to stale, triggers the checks to run again, and puts the fresh result in the same place. Proofs go stale as soon as the code changes; keeping them current is what this leg of the loop is for.

Turso, the team building a modern rewrite of SQLite in Rust, is one of our design partners; we wrote earlier about a durability bug we found in their engine. Their deployment shows what this leg of the loop looks like in practice. Every week, the machine-checked guarantees we maintain for them (currently 31, 17 of them on the page cache, and growing over time) are re-checked against the current revision and published as a report their team reads in plain English. When an upstream change breaks a guarantee, its row flips red the same week with a reproduction attached; when it is fixed, the row turns green and the check remains in place as a regression guard.

Where this leaves us#

The provers are ready, as results like seL4 and CompCert show. Adoption has been waiting on the loop's other two legs: specifications that developers can write and read, and results that reach them and stay current as the code changes. Build those two legs, and the provers we already have can finally be applied to the code that actually ships.

Aristo's core is free and open source. The full service, which takes claims all the way to machine-checked proof, is what we run with design partners, and we are onboarding 2 to 3 more: apply to join, or write to us at hello@aretta.ai.