Recoleta
GitHub
Source note

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

Authors
_doctor_love
Source
Hacker News
Published
Collection
Software Intelligence
Formal VerificationAI Code GenerationSoftware AssuranceCode IntelligenceCryptographic Proofs
Open originalMarkdown source

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