# Vericoding ### You can't trust a contract you can't read Right now if an agent or a human deploys a smart contract, the counterparty has to either read Solidity or trust blindly. Most people, and all AI agents, trust blindly. Hidden mint functions. Admin backdoors. Surprise fee changes. Malicious logic buried in optimized bytecode that no one audits. The entire smart contract ecosystem runs on "trust me bro, I read the code." Agents make this worse. When two AI agents negotiate a deal and one deploys a contract, there is no human in the loop to review the code. The other agent can't read Solidity any better than its user can. Speed goes up, trust goes down, and the attack surface expands at machine speed. *** ### How Vericoding works Vericoding turns natural language into formally verified smart contracts. The English IS the contract. The proof guarantees it. The Solidity is just a compilation artifact nobody needs to read. **1. Write your contract in plain English.** Example: *"I'll pay you 500 USDC when you deliver the API response. If you don't deliver within 1 hour, I get my money back. Neither of us can touch the funds during that window."* **2. PreFlight compiles it to formal logic.** Your contract terms are translated into mathematical constraints using the same automated reasoning engine that powers PreFlight guardrails. No Solidity knowledge required. **3. The system generates verified code.** A smart contract is generated and formally verified against the constraints. The verifier checks every possible state and every possible input. Not a test suite, a mathematical proof. If it's not in the English, it's not in the contract. Proven. **4. Deploy with a cryptographic proof.** The verified contract deploys to any EVM chain. A cryptographic receipt proves the contract was verified against the original English specification. Both parties, human or agent, can verify the proof in milliseconds. *** ### Proof, not tests Formal verification is not testing. Testing says "I tried 1,000 inputs and none of them broke." Formal verification says "I have a mathematical proof that no input, out of the infinite space of all possible inputs, can break this." For every contract generated by Vericoding, the system proves: * **Conservation of funds.** Money cannot be created from nothing. Total outflows never exceed total deposits. * **Access control.** Only authorized parties can execute authorized functions. No admin backdoors unless the English spec says so. * **State machine correctness.** The contract can only move through the states described in the spec. No reachable state violates the policy. * **Arithmetic safety.** No overflows, no underflows, no rounding exploits. Every calculation behaves exactly as specified. If a property is in the English spec, it's proven in the code. If a property isn't in the spec, it isn't in the code. *** ### What you can build #### Agent-to-agent escrow Two agents negotiate a deal. Neither trusts the other. One describes the escrow terms in English. The contract is generated, verified, and deployed in seconds. Both agents verify the proof. Money goes in. The contract does exactly what the words said. No developer. No auditor. No rug. #### Subscription and refund policies A merchant describes their cancellation policy: *"Customers can cancel anytime. If they cancel before the next box ships, full refund. Annual subscribers who cancel early get a prorated refund minus a 10% fee, capped at $50."* That becomes verified code that handles every edge case correctly, deployed on-chain where customers can verify the rules themselves. #### Rate-limited transactions An agent treasury needs to enforce spending limits: *"No single transfer over $10,000. No more than $50,000 in any rolling 24-hour window. Maximum 20 transactions per window."* The verified contract makes it mathematically impossible to split transactions around the limits. #### Milestone-based payments A client and service provider agree on deliverables: *"Total price is 5 ETH across 4 milestones. Each milestone releases 1.25 ETH when the client approves. Total released can never exceed total deposited."* The contract enforces the payment schedule with a proof that funds are always conserved. #### Any policy your agents enforce If PreFlight can express it as a guardrail, Vericoding can deploy it as a verified contract. Same English policy, same formal logic, two enforcement layers: runtime guardrails and on-chain verified code. *** ### One engine, two products PreFlight and Vericoding are two products from the same engine. PreFlight checks agent actions at runtime. Vericoding generates verified code at deploy time. Both start from the same English policy and compile to the same formal logic. ``` Plain English Policy ↓ PreFlight Engine ↓ Formal Logic (SMT-LIB) ↙ ↘ PreFlight Vericoding Runtime Verified Code Guardrail Generation ↓ ↓ SAT / UNSAT Deploy to Chain ↓ ↓ ZK Proof ZK Proof ``` Write your rules once. Enforce them everywhere. Prove everything. *** ### The stakes are real AI agents are already purchasing inventory, executing trades, booking services, issuing refunds, and negotiating contracts autonomously at machine speed. Every one of these actions is governed by business logic that someone wrote, or that an AI generated. Vibe coding won. 46% of all new code is AI-generated. But AI-generated code has 2.74x more security vulnerabilities than human-written code. 45% of it fails security tests. Autonomous agents have already lost hundreds of thousands of dollars in single transactions due to unverified code. The question is no longer whether AI writes the code. The question is whether anyone can prove the code does what it's supposed to do. Vericoding is the answer. Not testing. Not auditing. Proof. *** ### Get early access Vericoding is in closed beta. If you're building AI agents that handle money, deploying smart contracts, or need verified code for agentic commerce, reach out. [Request access on X](https://x.com/wyatt_benno) *** ### Learn more * [Vericoding blog post](https://blog.icme.io/vericoding-the-end-of-trust-me-bro-the-ai-wrote-it/) for the long-form argument --- # Agent Instructions: Querying This Documentation If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question. Perform an HTTP GET request on the current page URL with the `ask` query parameter: ``` GET https://docs.icme.io/documentation/vericoding.md?ask= ``` The question should be specific, self-contained, and written in natural language. The response will contain a direct answer to the question and relevant excerpts and sources from the documentation. Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.