Code that carries its own proof.
AI writes code faster than anyone can review it. Attestral is a machine-checked verification layer — any function, algorithm, or crypto / numeric / security routine I generate is compiled, linted, property-tested, and, where it matters, formally proved, then auto-revised from the checker's counterexample until it passes.
Internal tooling I built and run across my own projects — not a commercial product. Shown here as evidence of the engineering.The same principle, applied to code
Determinism, a proof you can reproduce, and a certificate anyone can re-run.
Machine-checked, locally
Every AI-generated function is checked before I trust it — compile, lint, and property-based tests — and, where it matters, a formal proof. Nothing leaves the machine.
Formal proof, six ways
Six formal rungs — Kani and CBMC (bounded model-checking), Lean 4 (kernel proof), Dafny and F* (SMT / dependent types), and TLA+ (design model-checking) — pick the strongest a given routine can carry.
Auto-revised from the counterexample
A refuted check is a task, not a result: the loop feeds the checker’s exact counterexample back and revises the code, up to three rounds, until it passes.
A certificate anyone can re-run
Every verified result carries a real ed25519-signed certificate under a published key. Anyone can re-run the same checker offline and reproduce the verdict — a deterministic proof, not a confidence score.
UNDER THE HOOD
Catch → Fix → Prove
A machine checker refutes wrong code deterministically; the refine loop auto-revises from the counterexample; and a signed, offline re-verifiable certificate proves the result. Not a confidence score — a proof.
Ten languages, one interface
Rust, Python, TypeScript, JavaScript, Go, C, Lean 4, Dafny, F* and TLA+ — each with a language-specific checker ladder, exposed through a single MCP verification tool any AI coding assistant can call.
10 languages · 6 with formal rungsFormal, not just tested
The formal rungs discharge correctness to a proof engine — Kani/CBMC symbolic model-checking, the Lean 4 kernel, Z3-backed Dafny and F*, and TLC for TLA+ designs — so a passing result means proven up to the stated specification, not merely un-refuted.
Kani · CBMC · Lean 4 · Dafny · F* · TLA+Signed, offline-verifiable receipts
A real ed25519 keypair (private seed local, public key published) signs a self-contained certificate for every verify. A shipped public verifier checks code integrity, receipt integrity, and signature — and re-runs the ladder to reproduce the verdict, trustlessly.
ed25519 · offline re-verifyA companion to the AI, not a rival
Claude or Cursor still writes the code; Attestral is the verifier it calls. That keeps the fast-generation loop while making its output provable — the deterministic slice of anti-hallucination, applied to code and math.
MCP tool · local-firstWhy a deterministic verifier
Hallucinated code shouldn't reach production. The formal rungs are airtight up to the specification; the behavioural rungs are as strong as the test — an honest, bounded claim. It's the same verifiable-systems pattern behind bitrep's bit-identical arithmetic and Cairn's trust decisions, turned on the code itself.
Built and running
The verification layer behind my own development — designed, built, and dogfooded daily. Internal tooling, not a product for sale.