What is vericoding?

The future of software engineering is undergoing a massive paradigm shift. With a plethora of low-cost, AI-driven programming tools at our disposal, the sheer volume of code being produced is reaching unprecedented scales. But this brings a critical problem: human review simply cannot keep pace. Traditional code review and manual testing fall short when an LLM can generate thousands of lines of code in seconds. We are shifting from an era where writing the code was the bottleneck to one where verifying its intent is the ultimate challenge.

What is Vericoding?

Vericoding, or AI-guided certified program refinement, is a modern approach to software engineering that ensures a program does exactly what it is intended to do. Rather than focusing on how a program is written, vericoding focuses on its specification, a formal description of its intended behavior.

At its core, vericoding relies on a combination of a theorem prover (the certifier, such as Rocq or Lean) and AI. In this model, developers write the specification (the surface or contract of the software), and the machine handles the implementation (the volume). Vericoding is not an all-or-nothing leap; it exists on a gradient. You can start with Behavior-Driven Design (BDD) like Gherkin scenarios, move up to executable runtime contracts using tools like specsaver, and ultimately graduate to mechanised proof using tools like axiomander, where a theorem prover universally guarantees the code behaves correctly across all possible inputs.

Why is Vericoding Important in the Age of AI-Generated Code?

In the age of AI vibecoding, where an LLM writes the code, you run a few tests, and ship it, the fundamental question remains: “What is this software supposed to do?”

When models write more code than humans can review line-by-line, attempting to understand a system just by reading the implementation means we are already lost. Vericoding solves this through the Holographic Principle for Software. Every function has a surface (preconditions, postconditions, and invariants) and a volume (the implementation). Vericoding enforces that the contracts at every interface tell you everything you need to know to reason about the system. The proof that the underlying volume obeys this surface is left entirely to the machine, cutting through AI-generated slop and ensuring that shipped code is robust, predictable, and correct.

Why AI Has Made Formal Verification Accessible to the Masses

Historically, automated formal verification and supercompilation (the process of replacing a program with a behaviorally equivalent but highly optimised one) hit a theoretical wall: Rice’s Theorem. There could never be a single sufficiently clever compiler that could optimise and verify everything without failing to terminate.

AI changes this radically by acting as an oracle. Instead of struggling to find a universal decision procedure, we can use an AI to speculatively guess faster programs, suggest transformations, and solve complex refinement steps. The theorem prover then acts as a strict judge, mechanically checking the AI’s guesses for behavioral equivalence against the specification. By decoupling the guessing (AI) from the checking (theorem prover), AI side-steps the theoretical limits that previously held back formal verification, making cheap, fast, and mathematically correct software accessible to boutique teams and enterprises alike.

How We Are Using Vericoding

At Scidonia, we use vericoding to prove what your program does and then make the slow paths faster. Here is a short overview of our specialized services:

• C & Rust Speedup: We cut latency in C and Rust services and use theorem provers to guarantee the highly-optimized result still flawlessly meets its original specification — or you pay nothing.
• Database Speedup: We compile high-volume queries and formally prove that they return the exact same rows, values, and errors as your original database setup.
• Faster Spatial Queries: We compile high-volume spatial (GIS) queries and prove they return exactly what the database returns, just drastically faster.
• API Workflow Verification & Faster Gateways: We check workflows spanning several systems to find late events, cancellations, or retries that leave payments or access in the wrong state. We can also specialise an API gateway to a fixed configuration and prove it still meets its specifications.
• Verified Security: We prove a reusable security component once, and then automatically adapt that mathematical evidence for every product that uses it.
• Document Workflow: We cite each fact from a source document and formally check the workflow that passes it to subsequent processes.

Ready to Verify?

We are providing vericoding consultancy to help teams bridge the gap between AI vibecoding and verified software. Get in touch with Scidonia to help get you started proving your code does what you and your users expect.