Technical knowledge for building provably correct systems

Deep dives, implementation guides, research, and real-world verification insights for engineers working on complex software.

Better softwareA more open world

Search articles

Filtering by:AI & Automation

Quick links:AI & Automation Blockchain Infrastructure Formal Verification Institutional Finance

Subscribe to updates ↗

Results

2 articles

Sort articles

AutoProver vs Human Verification blog image

AI & Automation

Technical Case Study

We spec'd the Aave v4 Hub by hand. Then we let AutoProver try

Certora compared AutoProver’s independently generated Aave v4 Hub specification with a human-authored verification engagement. AutoProver discovered and proved substantial solvency and accounting properties, but the comparison also revealed why generated coverage must be paired with expert analysis of protocol intent and economic safety.

August 20, 2026Read article ↗

AI & Automation

Technical Analysis

Concordance: Automatically Simplifying Smart Contracts

Concordance is an open-source tool that uses LLMs to automatically rewrite heavily optimized Solidity (including inline assembly) into clear, readable code while preserving all observable on-chain behavior. Each rewrite is proven equivalent by Concord, the equivalence checker, so audits get easier without sacrificing correctness.

September 12, 2025Read article ↗

Explore by topic

View all topics →

AI & Automation
Blockchain Infrastructure
Formal Verification
Institutional Finance
Operational Security
Product & Company
Smart Contract Security

Get Certora's latest engineering research.

Email address