Gain trust from AI generated code again with semantics constract

bz

Jul 17, 2026

💡 TL;DR Notice AI writes code faster than humans can review it, creating a massive trust crisis. Unit tests and prompt engineering aren't enough. Here propose Semantic Contracts—a type-safe, compile-time blueprint that sits between your requirements/prpmpts and code, guaranteeing correctness no matter who (or what) wrote the implementation.

AI-driven development (often called “Vibe Coding”) has massively boosted our coding speed. However, because we don’t truly know how AI models make their decisions, we are facing a fundamental crisis of trust.

This paper proposes a practical solution: Semantic Contracts.

A semantic contract is a structured, verifiable blueprint of your core business logic. Positioned right between raw human requirements and actual code, it uses typed states, simple building blocks (combinators), and compile-time checks to guarantee that any implementation—whether written by a human or generated by an AI—is automatically trustworthy as long as it fits the contract.

In this blog, I describe what semantic contracts are, explain their math-like building blocks, demonstrate them using sorting algorithms and e-commerce checkout examples, and discuss how they can plug into your existing systems.

1. The Problem: How AI Broke the Software Engineering “Chain of Trust”

In the pre-AI era, software engineering relied on a highly structured pipeline to build trust:

Requirements → Architecture → Detailed Design → Coding → Testing → Code Review → Deployment

Every step had clear inputs, outputs, and human ownership. We trusted the software because we trusted the process. Even if we couldn’t mathematically prove the code was 100% bug-free, we had confidence because it went through multiple rounds of human review and automated testing.

In the AI era, this entire pipeline has collapsed. With “Vibe Coding,” you type a prompt, and the AI immediately spits out running code. The middle steps are gone. While we try to catch up with techniques like prompt engineering or automated test harnesses, the path from a user’s prompt to the final code remains a black box. Relying purely on AI self-correction or quick human reviews is, frankly, wishful thinking.

This shift has broken our chain of trust in four ways:

Unknown AI Behavior: AI code comes from neural networks with hundreds of billions of parameters. We cannot fully predict or understand it. The exact same prompt can yield completely different code under the hood.

Untraceable Bugs: When AI code fails, it’s incredibly hard to trace the failure back to a specific design flaw or logical error.

Unpredictable Fixes: Prompting an AI to fix one bug can easily introduce unexpected side effects elsewhere.

Impossible Code Reviews: Humans simply cannot review code as fast as AI can write it. Reviews quickly become a checkbox exercise.

If we cannot solve the question of “how to trust AI-generated code,” the massive speedups from AI will always come with risks we cannot afford to take.

1. The Solution: A Verifiable Bridge Between Ideas and Code

To fix this, we need a new layer in our workflow. It must be:

Between Requirements and Code: More precise than vague human language, but more abstract than actual code.

Guaranteed to Work: Any code that matches this layer must behave exactly as intended.

Composable: You can snap smaller pieces together to build larger systems.

Checked at Compile-Time: Errors should be caught by the compiler, not during runtime.

I call this Semantic Contracts.

While semantic contracts are not exclusive to AI, they are highly effective at preventing AI “hallucinations” because they strip away irrelevant details and enforce strict types. If an AI generates a bad implementation, the compiler will simply refuse to build it.

💡 A simple analogy:

Imagine the classic joke of putting an elephant in a fridge in three steps:

Open the fridge.

Put the elephant in.

Close the fridge.

A semantic contract guarantees that these three steps happen exactly in this order. It secures the process, even though it doesn’t verify if the elephant actually fits inside.

1. Why Existing “Formal Methods” Failed

Computer scientists have tried to prove program correctness for decades (using tools like Hoare Logic, Z language, or Model Checking). Yet, they never went mainstream because:

They focus on “finding bugs” rather than “building things right.” Traditional methods try to verify code after it is written. That is passive and incredibly hard. We want to make correctness a natural byproduct of how we build the code in the first place.

Writing specifications is too hard. Writing perfect mathematical rules for a complex business system is often harder and more exhausting than writing the actual code.

The State Explosion Problem. Verifying large programs requires checking astronomical numbers of possible pathways, which quickly crashes even the best verification tools.

Our approach does not try to “prove everything.” Instead, it focuses on process guarantees. By using structured building blocks, your code becomes correct by design, not by coincidence.

1. What is a Semantic Contract?

4.1 The Blueprint

A semantic contract is a structured, verifiable description of a business operation. It consists of three parts:

Rust

contract Name(input_state) : output_state = structural_definition with Capability { ... }

contract Name(input_state) : output_state (The Signature): Defines what state goes in, and what possible states can come out.

= structural_definition (The Skeleton): An expression tree made of basic building blocks (combinators).

with Capability (The Extra Powers): Attaches behaviors like database transactions, retries, rate-limiting, or logging.

Once defined, any contract can easily be reused inside other contracts.

4.2 “States” are the Only Results

Instead of throwing random errors, our contracts return explicit “States.” A state is a simple data structure that carries information:

Success(TransactionId) | InsufficientBalance(available: Money) | Processing(Token) | Blocked

If your business rules are violated (e.g., trying to transfer negative money), you don’t throw an exception. You simply return an InvalidAmount state.

Handling “Uncaught” States (Exceptions):

By default, contracts have two basic states: Success and Fail. If a contract returns a custom state (like InsufficientBalance) and the next step doesn’t explicitly handle it, the compiler treats this as an “unhandled exception.” It will then:

Pass it up if the parent contract can handle it.

Throw a compile-time error if nobody handles it. This forces developers (or AI) to handle every edge case before the code can even run.

4.3 The Building Blocks (Combinators)

We use a small set of predefined operations to chain business logic together:

Seq: Run A, then B. If A fails, stop and return the failure.

Par: Run A and B at the same time. Both must succeed.

Batch: Run operation A on a list of items, one by one.

Race: Run A and B. Return whoever finishes first.

ScatterGather: Split a task, run in parallel, and merge results.

Transaction: If step B fails, roll back step A.

Timed(duration, A): A must finish within the limit, or it fails.

This maybe not a complete list to support all common cases, but they are powerful enough to represent most any business workflow. As they have predictable math-like rules, the compiler can easily check if your pipeline makes sense.

1. Example 1: A Sorting Algorithm

Let’s see how a standard sorting algorithm looks as a semantic contract.

5.1 Defining the Contract

First, we define our “trusted foundation tools” (atomic operations):

contract CheckSorted(List) : Sorted(List) | Unknown(List) = Trusted_Atomic_Operation

contract Partition(List) : Success(Less: List, Greater: List) | Failed(Error) = Trusted_Atomic_Operation

contract Merge(List, List) : Success(Sorted: List) | Failed(Error) = Trusted_Atomic_Operation

Now, we define the actual sorting process:

contract Sort(List) : Success(Sorted: List) | Failed(Error) = Seq Success(list), Unknown(list) -> Seq, Merge(sorted_less, sorted_greater) > } >

5.2 Why This is Guaranteed to Work

The structure of the contract makes it impossible to fail:

Check: If the list is already sorted, return it immediately (this handles empty or single-item lists, stopping the recursion).

Divide: Split the list into “less than” and “greater than” piles.

Sort: Run sorting on both halves in parallel.

Merge: Combine the results.

This contract assumes the atomic tools (Partition and Merge) work correctly. How we guarantee those works is a separate issue (via unit tests or formal proof), but the overall assembly of our sorting algorithm is 100% verified by the compiler.

Note how for a pure math problem like sorting, the contract is essentially the algorithm itself. For business applications, however, contracts behave differently.

1. Example 2: E-Commerce Checkout

Let’s design a real-world checkout system where we need to charge a user and deduct inventory.

contract PlaceOrder(AccountId, List) : Success | Failed(Error) = Seq

6.1 Adding Edge Cases (Refining the States)

Payments can fail due to low balances; items can be out of stock. Let’s make these outcomes explicit:

contract Payment(AccountId, Money, OrderId) : Success(TransactionId) | InsufficientBalance(available: Money) | Failed(Error)

contract Inventory(OrderId, List) : Success(List) | InsufficientStock(item: ItemId, available: Quantity) | Failed(Error)

Now, we update our main PlaceOrder contract. The compiler will force us to include these new potential failure states in the main output:

Rust

contract PlaceOrder(AccountId, List) : Success | InsufficientBalance(available: Money) | // From Payment InsufficientStock(item: ItemId, available: Quantity) | // From Inventory Failed(Error) = Transaction>

6.2 Zooming In

Let’s define the steps inside Payment and Inventory:

contract Payment(AccountId, Money, OrderId) : Success | InsufficientBalance(available: Money) | Failed(Error) = Seq

contract Inventory(OrderId, List) : Success(List) | InsufficientStock(item: ItemId, available: Quantity) | Failed(Error) = Batch

6.3 Adding New Features

What if we want to send an email notification after a checkout attempt, regardless of whether it succeeded or failed? We can update the parent contract like this:

contract PlaceOrder(AccountId, List, Email) : Success | InsufficientBalance(available: Money) | InsufficientStock(item: ItemId, available: Quantity) | Failed(Error) = Transaction { _: SendNotification }

This showcases the natural engineering process: starting with a high-level concept and gradually adding detail. Traditional design documents try to do this but lack compiler validation; code has the compiler but hides the big-picture design. Semantic contracts bridge this gap perfectly.

1. Elevating Logic to Types

The core idea here is to treat business logic as a type system.

In traditional programming, business rules are buried inside nested if/else statements, database calls, and error-catching blocks. There is no automated way to prove that they all play nice together.

Semantic contracts turn “payment” into a set of strict, typed rules. When everything is typed:

You can plug things together: Payment can be safely used in any larger checkout system.

You can verify it instantly: The compiler checks if your logic matches your blueprint.

You can swap implementations: Any code that satisfies the Payment contract can be swapped in without breaking the system.

It replaces messy, ad-hoc if/else spaghetti with compile-time guarantees.

1. Plugs and Play: Integrating with Existing Systems

Most existing codebases do not have semantic contracts. How do we adopt this?

Here we define a Hierarchy of Trust:

Infrastructure Trust: Low-level components like the Linux Kernel, TCP/IP, or PostgreSQL. We assume these work correctly because they are battle-tested by millions of

[truncated for AI cost control]