---
source: hn
url: https://blog.icme.io/vericoding-the-end-of-trust-me-bro-the-ai-wrote-it/
published_at: '2026-05-24T22:07:38'
authors:
- _doctor_love
topics:
- formal-verification
- ai-code-generation
- software-assurance
- code-intelligence
- cryptographic-proofs
relevance_score: 0.92
run_id: materialize-outputs
language_code: en
---

# Vericoding: The End of "Trust Me Bro, The AI Wrote It"

## Summary
The article argues that AI code generation has outpaced code verification, and it proposes a product path that turns natural-language intent into formal specs, verified code, and cryptographic proof artifacts.

## Problem
- AI coding tools generate code faster than teams can review it, which matters because security, compliance, and correctness checks become the bottleneck.
- The article cites higher defect and security risk in AI-written code: 2.74x more security vulnerabilities, 45% security-test failure, and 3x faster technical-debt growth.
- Existing vericoding work often starts from a formal specification, but most developers and domain owners write requirements in natural language.

## Approach
- The proposed pipeline starts with natural-language intent, then uses multiple LLMs to translate it into Dafny-style preconditions and postconditions.
- Z3 checks the generated spec before code generation, looking for consistency, underspecified cases, and inputs with undefined behavior.
- A human reviews the spec gaps rather than reviewing a large code diff.
- An LLM generates a Dafny implementation, and Z3 verifies that the code satisfies the spec.
- The system archives SMT-LIB2 proof artifacts and wraps verification results in cryptographic receipts for third-party audit.

## Results
- The cited vericoding benchmark covers 12,504 formal specifications across Dafny, Verus/Rust, and Lean, with up to 82% success in Dafny using off-the-shelf LLMs.
- The article says pure Dafny verification improved from 68% to 96% over the past year, and cites DafnyPro at 86% first-pass success.
- It cites AWS Cedar verification in Dafny for an authorization engine handling over 1 billion API calls per second, with differential testing against quadrillions of production authorizations and a 65% performance improvement.
- The article claims the market pressure is large: 92% of developers use AI coding tools daily, 46% of new code is AI-generated, and Gartner forecasts 60% of new software code will be AI-generated by the end of 2026.
- It does not provide a new quantitative evaluation of ICME’s proposed end-to-end natural-language-to-verified-code system; the strongest concrete claim is that PreFlight already translates natural-language guardrail policies into formal logic and checks them with an SMT solver in under a second.

## Link
- [https://blog.icme.io/vericoding-the-end-of-trust-me-bro-the-ai-wrote-it/](https://blog.icme.io/vericoding-the-end-of-trust-me-bro-the-ai-wrote-it/)