From intent to guarantee.Your agent writes the code.Aristo proves it holds.

Aristo is Aretta’s verification SDK: verifiable intent, inline with your code. You declare the property that matters, right above the function. Aristo checks whether the code can break it, and flags drift the moment code and claim diverge.

get aristosee it in action ↓
src/range.rs✓ Verified · neural
/// Clamp `value` into the inclusive range `[lo, hi]`.
#[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 problem

AI writes your code. Nobody can prove it works.

Every team is shipping AI-generated code. But the verification story hasn't changed — you still write tests by hand, review line by line, and pray nothing slips through.

The faster you generate code, the faster you generate bugs. Your bottleneck isn't writing code anymore. It's trusting it.

aristo sdk

Verification, inside your agent's loop. No new tool to learn.

Aristo ships as skills your coding agent already knows how to use. Watch Claude Code author a claim, verify it, and catch the exact moment a refactor breaks it.

Claude Code — ~/dev/acme-db
✳ Claude Code · aristo skills installed
1 · the agent writes the claim with the code
>Add a clamp helper that keeps a value inside [lo, hi], and claim it.
⏺Writing src/range.rs with an #[aristo::intent] claim above the function…
#[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) }
⏺Bash(git commit -m "Add clamp with range claim")
→ Found 1 annotations · new: 1, unchanged: 0, body-drifted: 0 ok: stamped 1 annotation into .aristo/index.toml
2 · verify: the claim holds
>/aristo-verify
Scope × mode · Changed · neural (default · local · no sign-in)
✓ clamp_in_range · Verified (neural)
Claim returns a value within [lo, hi] for any input
Held with lo <= hi assumed, max(lo) enforces the lower bound and .min(hi) caps the result; both bounds hold.
3 · a refactor drifts from the claim
>Perf tweak: drop the upper-bound check, callers guarantee hi.
⏺Edit(src/range.rs) · value.max(lo).min(hi)
● clamp_in_range · body changed
status was Verified, now Stale
4 · re-verify: the claim is refuted
>/aristo-verify
✗ clamp_in_range · Refuted
Claim returns a value within [lo, hi] for any input
Found the function returns value.max(lo), which has no upper bound; for value > hi the result exceeds hi, violating the claim.
Verify done · ✓ 0 verified · ✗ 1 refuted · ? 0 inconclusive · caught before the change shipped.

Declare

One plain-English claim above the function. Your agent writes it as it works.

Verify

A free local critic checks every edit; tests, fuzzing, and formal proof for the guarantees that matter.

Catch

Code drifts, claims notice. A broken claim flips loudly, before the change ships.

design partnership

You specify. Aristo proves.

Aretta takes the claims that matter most all the way to machine-checked proof, and keeps score on one dashboard: what holds, at what rigor, and exactly what broke. As part of our initial launch we are onboarding 2 to 3 more design partners. Below: a real dashboard from an anonymized partner deployment.

apply to join
●acme-db.aretta.ai/overview

Verification posture

adept  week of Jul 18, 2026
31
machine-checked guarantees
1
finding · caught & fixed upstream
0
open divergences
3
subsystems under contract
held rate
31 / 32 · 97%
guarantees by subsystem · page cache 17 · wal 7 · storage & vacuum 7
WALA commit frame must reach stable storage via fsync before the transaction is reported as durableproofHELD
WALWAL truncate is atomic: no committed frame is lost across the truncate operationproofHELD
Page CacheA pinned page is never evicted while any cursor still references ittestHELD
Page CacheThe evictable-page count never drifts from the true number of evictable pagesproofDIVERGED → FIXED
× PROPERTY VIOLATED · pagecache_evictable_count fixed upstream
impl core/storage/pager.rs
divergence expected evictable = 12 (reference) · actual 13 (engine)
why the add-dirty guard double-counts a page returning from spill
reproduce aristo verify --filter id=pagecache_evictable_count --rerun

the team

From Berkeley's lab to every line you ship.

Aretta is founded by formal methods researchers from UC Berkeley. We built the verification techniques that live in academic papers — now we're shipping them as infrastructure that works at production scale. The frontier of correctness, available to every team.

Adwait GodboleCo-Founder & CTO

PhD, UC Berkeley. Formal methods + GenAI.

C. V. Ramamoorthy Distinguished Research Award.

Sushant DineshCo-Founder & CEO

PhD, UC Berkeley. Scalable verification.

Best paper award for scaling formal methods to large systems.

backed by

Sanjit A. Seshia — Founding Advisor

Cadence Founders Chair Professor of EECS, UC Berkeley

Ion Stoica — Advisor

Co-founder Databricks, Anyscale, LMArena, Conviva

Xu Bao Chancellor's Chair and Director of SkyLab

Kurt Keutzer — Advisor

Former CTO of Synopsys, Co-founder DeepScale (acq. Tesla), Nexusflow (acq. NVIDIA), Narada

Professor Emeritus, UC Berkeley

Stop reviewing. Start verifying.

Aristo's core is free and open source. If a wrong answer on the failure path is unacceptable for what you build, we would love to talk.

apply to joinhello@aretta.ai →