Correctness by Construction in the AI Age

Correctness by construction in the AI age means moving trust out of the assistant and into compilers, hooks, macros, CLIs, tests, and gates that make bad output unshippable.

It matters more now than it ever did before. At first glance the two ideas seem like antonyms. The obvious objection is this: how can anything be correct by construction when the same prompt fed to the same model can produce a different reply tomorrow? When model quality drifts as compute scales up or down?

AI agents are not magic. Prompting an AI to write the right code is only as reliable as the constraints around the request. In my consulting experience, and quite honestly in my own code-writing experience, you can have 50 stand-up meetings dedicated to code quality, deny 50 PRs, and hand everyone the same architecture books. People still forget, get lazy, miss context, or simply do not see the value. Agents fail differently, but the lesson is the same: advice is not enforcement.

At the time of writing this article, the idea of agents writing all code is a fallacy, but the idea that agents can only write slop is a far more egregious one.

You Must First Invent the Universe

To steal the Carl Sagan line: "If you wish to make an apple pie from scratch, you must first invent the universe."

We are going to do our own version of that. That is to say, we are going all the way down to first principles with this one.

Before hooks, skills, agents, or even language choice, we need to ask why we are writing code at all.

Code gives us speed, obviously. The deeper value is repeatability: the same input should produce the same behavior, the same way, every time.

A pacemaker cannot usually decide correctly. Flight-control software cannot improvise on the millionth loop because it got tired or inspired. The whole point of putting the rule in code is that the same input should hit the same rule, the same way, every time, at machine speed. If there is any chance of variability where determinism matters, it is instantly a non-starter.

If we want AI agents to scale, we have to drag them toward that same standard: fewer vibes and a repeatable path from instruction to acceptable output.

The language is where the agent's universe begins.

So the first question is: what language are we writing in?

Do the mental experiment even if you already know the answer. Do it even if you have a project in your head right now and you are unwilling to switch languages. Do it even if you only know one language at this exact moment.

The language is paramount. Yes, we are going to get into guardrails inside your AI harness, but the compiler has to do as much work as you can possibly make it do. The important rules need to live somewhere with teeth.

Wherever possible, use a type-safe language with strong opinions. If you are using libraries inside that language, use opinionated libraries too. Avoid libraries altogether when that is the correct shape for the problem. If you must use them, pick libraries that are strict about correctness and make nonsense hard to express.

Choosing your language gives you better guardrail material later. The languages I reach for are:

• TypeScript, especially if you are a beginner or not as confident in other languages. Everyone has to learn TypeScript and all its baggage, for better or worse, so I am obligated to say it first, and it brings me no joy to do so.
• Rust, because the compiler acts exactly how you would expect from a language this obsessed with correctness. The ecosystem also has serious libraries, lints, and macro surfaces that let you push those rules into your domain model.
• Haskell, because a suspicious number of the best ideas in other languages trace back to it. The only "downside" is that it can be too opinionated sometimes, but for this argument, that is the point.

There are plenty more, but the decision matrix is this: what does compiling tell me? In Haskell, Rust, Agda, Coq, and languages in that neighborhood, the type system can encode invariants, preconditions, invalid state transitions, and sometimes whole specifications. Compilation starts acting like a proof check. If it passes, you have ruled out null dereferences, data races, missing cases, impossible states, and, depending on how far you pushed the types, even some logic errors. In a language like TypeScript, compiling can tell you almost nothing if you let it. The closer you get to the proof-checker end of that spectrum, the better.

The examples below stay mostly in Rust and TypeScript because those are the surfaces I live in most. Once the universe has better physics, the next job is making the good path easier than the bad one.

Pit Before the Prompt

The pit of success is the right mental model here. The AI needs to fall into it. I did not coin that term, but it is the best programming idiom I know for this exact problem. It extends almost perfectly to AI.

The original 2003 idea is usually credited through Brad Abrams' writing, with Rico Mariani named as the person who coined the phrase. The cleaned-up version to read is The Pit of Success on The Philosopher Developer, because the old MSDN version is not exactly a joy to read in the modern internet ruins.

That idea was aimed at developers: design APIs so the right thing is the natural thing, and the wrong thing is hard to reach. Some people would call that "opinionated," but opinionated can mean opinionated in the wrong direction. The point is to make the bad move hard to make in the first place.

That same idea matters even more when you are working with AI. Humans miss context. AI can invent context and present it like gospel. Choosing the right language pushes it closer to the pit of success before the agent touches the codebase at all.

Skills help too. If you have never used them, start here, but the short version is this: Claude reads skill files the same way users read Terms of Service; sometimes, and often not at all. A skill is a nudge in the right direction.

Agents often follow skills pretty well these days, especially when a skill is invoked directly. The issue is that skills can drift. Skills are sort of like code in my eyes: they need upkeep. What they give us is a way to fill in the gaps where we cannot be fully deterministic, but they are not enforcement.

So "just use this skill and your agent will never hallucinate again" is out. What is in?

From there, suggestions stop being enough. Enforcement has to enter the picture.

Hooks >

Hooks are the only thing in the agent stack that actually scales. Multi-agent workflows need hooks. Agent orchestration needs hooks. Smaller local models need hooks. The rest of the stack gets useful because hooks force every write through the same rules; without them, the workflow either stops scaling or becomes unusable unless a human is constantly in the loop.

A smaller model will not reason as well as the expensive one most of the time. For real work, local agents are not viable by default. In specific domains, with the right set of hooks, they become usable because the hooks constrain the output harder than the model ever will on its own.

That opens up a lot of workflows. You can have a high-level agent do the reasoning, design the change, and hand the implementation to a worker. Without hooks, that worker might write something like this:

type SaveUserResult = {
  // Boolean state makes the caller reverse-engineer which fields are valid.
  ok: boolean;
  // These optionals allow nonsense like `{ ok: true, error: "bad" }`.
  user?: User;
  error?: string;
};
 
// `any` means the compiler has clocked out. Have fun debugging `user.id`.
async function saveUser(user: any): Promise<SaveUserResult> {
  try {
    return { ok: true, user: await db.users.save(user) };
  } catch (error) {
    // Every failure becomes a string: database, validation, permission, all soup.
    return { ok: false, error: String(error) };
  }
}

The sloppy version is much faster to type. It is fewer tokens for the agent to spit out. Depending on the size of your project, it can even get the product shipped sooner.

Then it's 3 a.m. This works fine as long as nothing ever changes. Something does change, in exactly the wrong way, and now you have a stringly typed error message while you have paying users and a contract to fulfill. Enter: the pit of despair. In my personal experience, I can safely say the "speed gains" have never been worth the sanity losses from writing "pragmatic" code.

With the right hooks, the agent gets forced into this kind of shape:

type SaveUserFailure =
  | {
      kind: "ValidationFailure";
      field: "email" | "displayName";
      message: string;
    }
  | {
      kind: "PermissionFailure";
      requiredRole: "Admin" | "Support";
    }
  | {
      kind: "DatabaseFailure";
      operation: "insertUser";
      retryable: boolean;
    };
 
type SaveUserResult =
  | {
      kind: "Saved";
      user: User;
    }
  | {
      kind: "Rejected";
      failure: SaveUserFailure;
    };
 
async function saveUser(user: NewUser): Promise<SaveUserResult> {
  const validation = validateUser(user);
 
  if (validation.kind === "Invalid") {
    return { kind: "Rejected", failure: validation.failure };
  }
 
  const savedUser = await db.users.save(validation.user);
 
  return { kind: "Saved", user: savedUser };
}

Now you get to know what happened. The caller switches on kind, the error carries the domain reason, and the compiler can tell you when you forgot to handle a case. If your hooks block the sloppy shape, the write bounces. The agent has to try again.

This does not have to start as some giant internal platform either. A tiny pre-commit hook can already prove the point:

#!/usr/bin/env node
import { execFileSync } from "node:child_process";
import { readFileSync } from "node:fs";
 
// Only inspect staged TypeScript files, because this hook is a file-boundary gate.
const stagedFiles = execFileSync("git", ["diff", "--cached", "--name-only", "--diff-filter=ACM"], {
  encoding: "utf8",
})
  .split("\n")
  .filter((file) => file.endsWith(".ts") || file.endsWith(".tsx"));
 
const bannedShapes = [
  {
    name: "`any` turns the compiler into interior decoration",
    pattern: /\bany\b/,
  },
  {
    name: "`ok: boolean` means a domain outcome got crushed into a light switch",
    pattern: /\bok\s*:\s*boolean\b/,
  },
  {
    name: "`String(error)` erases the failure type right when you need it most",
    pattern: /catch\s*\([^)]*\)\s*{[\s\S]{0,300}\bString\(/m,
  },
];
 
let failed = false;
 
for (const file of stagedFiles) {
  const source = readFileSync(file, "utf8");
 
  for (const shape of bannedShapes) {
    if (!shape.pattern.test(source)) continue;
 
    failed = true;
    console.error(`${file}: rejected: ${shape.name}`);
  }
}
 
if (failed) {
  process.exit(1);
}

Production hooks need to be smarter than this. They should parse syntax where possible, inject useful context, and avoid yelling about test fixtures or generated files. The important part is the control point: the write does not get to land just because the agent sounded confident.

The worker will run into issues. It will waste a few tokens, but depending on where you run your agent, that cost may not matter very much. If the worker is local, you are paying with time instead of API spend. Across enough implementation work, that workflow can save serious money.

The same thing applies when you are using a high-level agent like Codex directly. The benefits get absurd. You can use the /goal loop and trust that the code will land somewhere inside the bounds you permit. You can review PRs with less paranoia when a good set of hooks is blocking non-idiomatic code, or whatever your project defines as non-idiomatic code.

This even lets you do something I do not recommend: write in a dynamically typed language and claw back some structure with hooks. In Lua, for example, a hook could block this sort of magic-string workflow:

function charge_user(user, amount, mode)
  -- `mode` is free text, so every typo becomes a new unofficial state.
  if mode == "test" then
    -- `nil` means "test skipped" only if every caller memorizes the convention.
    return nil
  end
 
  if mode == "live" then
    return payment.charge(user.id, amount)
  end
 
  -- `false` is a second failure language. Very generous. Very cursed.
  return false
end

That is exactly the kind of thing you can refuse at the file boundary: magic string modes, nil as a domain result, false as a second failure shape. With enough of those checks, Lua starts feeling closer to TypeScript. Then TypeScript starts feeling closer to Haskell.

Force the agent toward this instead:

-- Named modes make the accepted inputs visible in one place.
local ChargeMode = {
  Test = "test",
  Live = "live",
}
 
-- One result tag gives callers a single field to switch on.
local ChargeResultKind = {
  Skipped = "skipped",
  Charged = "charged",
  Rejected = "rejected",
}
 
function charge_user(user, amount, mode)
  if mode == ChargeMode.Test then
    -- Test mode is a real result, not a secret `nil` convention.
    return { kind = ChargeResultKind.Skipped }
  end
 
  if mode == ChargeMode.Live then
    return {
      kind = ChargeResultKind.Charged,
      receipt = payment.charge(user.id, amount),
    }
  end
 
  -- Unknown mode is named as a rejection instead of hiding behind `false`.
  return {
    kind = ChargeResultKind.Rejected,
    reason = "unknown_charge_mode",
  }
end

Every branch returns the same outer shape, the result says what happened, and the caller can switch on kind instead of praying that nil means "test" and false means "something else went sideways, enjoy."

When the same bad shape keeps coming back, the hook can inject context right at failure time: "You used string modes. Use a discriminated union." The next attempt gets the relevant rule at the exact moment the model needs it.

In real projects, hooks reject shapes like these:

- Rust code reaching for `unwrap`, `expect`, `panic!`, or `todo!` at a domain boundary: rejected
- Rust APIs collapsing domain states into `bool`, `Option`, or string modes instead of an enum/newtype: rejected
- Haskell exports using partial functions like `head`, `tail`, `fromJust`, `!!`, or unguarded `read`: rejected
- Haskell pattern matches hiding future constructors behind a catch-all wildcard: rejected

Now imagine putting hooks around Haskell. It is already one of the strongest languages for encoding correctness into the type system. Hooks let you push those rules even further into the workflow.

That is the abstract version. The practical version is what we try to do inside Jakuta.

Festina Lente

At Jakuta Inc., agentic development is something we really pride ourselves on. Our internal development saying is festina lente: make haste slowly. Oxymoronic, yes, but in a poetic way. These two concerns are just as important, and they have to coexist.

The point is to use AI for the speed while shoring up the gaps AI opens. Speed is only valuable if the codebase survives the acceleration.

So for this goal, what better language to write most of our backend in than Rust?

Here is a real example from our Rust crates, trimmed to the shape:

// One declaration owns the HTTP status and the response body.
declare_jakuta_response! {
    pub Ok200 ExampleHealthResponse {
        message: ExampleHealthMessageText,
    }
}

That macro owns the response shape. The older escape hatch was letting authors compose derives and attributes by hand. That gives humans and agents too many places to be clever. The macro surface turns it into one declaration: name the response, name the fields, and let the crate generate the repetitive contract code.

The macro owns the item, the derives, the schema traits, the wire traits, and the constructor shape. The author does not get to quietly smuggle a bad attribute through the side door.

The real test of a pattern is not whether it looks clean in a toy example. It is whether it kills the next bug before it becomes a habit.

Human and Agent Proofing

The response-header case is a better example of the actual bug cycle:

// Header-writing responses use a separate macro with required slots.
declare_jakuta_response_with_headers! {
    Ok200 MyLoginResponse {
        body = MyLoginBody,
        headers = MySetCookieDirective,
    }
}

At one point, header-writing responses could be expressed through magic field names in the general response macro. That worked until it didn't: the body/header contract was implicit. The fix was to split header-writing into its own macro, where a header response has to name its body and headers explicitly. The grammar stopped letting the mistake exist.

The macros did not appear out of nowhere. They were built on top of hooks and gates that stop AI from writing unperformant code, runtime panic paths, and escape-hatch Rust that technically compiles while violating the project contract. The workspace lints deny unwrap, expect, panic!, todo!, dbg!, lossy casts, undocumented unsafe blocks, wildcard enum match arms, and a pile of other nonsense. jakuta-contract check backs the shared surface with a banned-shape catalog, drift checks, and contract self-audits.

Those shared crates show up across our backend work, from telemetry products to consumer-facing products. Developers and agents alike are forced toward the pit of success when they write Rust against those surfaces.

Whenever we patch a bug, we ask how the architecture allowed the bug to be written:

• The macro was not opinionated enough.
• The hook was not opinionated enough.
• The automatic PR hooks and gates were not consistent enough.

That is the response-header lesson in miniature: fix the bug, then remove the shape that allowed the bug.

At this point, the Rust macro story turns back into basic programming discipline.

This is really just DRY with sharper teeth. One of the first things I learned when I was learning programming was DRY: don't repeat yourself. It is the most important rule in programming.

Why? Because you do not want to fix the same bug ten times. The eleventh copy always exists somewhere, and now you have another runtime issue to debug.

We have extrapolated that idea as a company. The target is the whole class of footgun across the company. One file or one codebase at a time is too small. A crate updates, Cargo pulls the new version, and the bad shape disappears everywhere that depends on it.

That is why this macro matters to us, and why the pattern matters more than this one macro. It starts with picking the right language. Rust lets us build these kinds of macro surfaces, and that matters because Rust is useful across almost every backend we care about: hardware-adjacent systems, game services, financial services, company products, and personal projects. Rust gives us a correctness-oriented language we can bet on for most of the work we do.

Then the hooks empower the AI to work inside that world in the first place. The hooks push the agent toward the macro. The macro makes the right thing the only thing to do. That is a far cry from the usual loop:

• Check for the wrong thing after the fact.
• Deny the wrong thing after it already became a pattern.
• Advise against the wrong thing and hope the agent cares.

The remaining problem is that a macro only helps when the agent actually uses it.

Executable Contracts

The next objection is obvious:

"Hypothetically, what if the agent decides not to use the macro?"

Rest assured, the AI agent will find ways so nuanced and magical to do everything besides the thing you wanted that you almost want to give it a round of applause.

Hence: assume the AI is almost a bad actor. It will try to do the lazy, bug-ridden thing. So the next thing I did was make hooks that detect Rust projects and force the Jakuta contract CLI into the workflow. This is automated. There is nothing for an agent or a human to remember.

# Fix compile-blocking contract violations first.
jakuta-contract check --severity breaking --summary
 
# Group remaining Rust / TypeScript / Dart contract issues.
jakuta-contract check --targets rs,ts,dart --summary --group-by category
 
# Run the full contract gate.
jakuta-contract check --targets rs,ts,dart
 
# Discover the blessed surface before hand-rolling one.
jakuta-contract surface "wire body"
jakuta-contract usage declare_jakuta_wire_body
jakuta-contract why ApiRequest
 
# Compare the consumer contract against the current shared surface.
jakuta-contract whats-new --with-check --targets rs,ts,dart
 
# Check the file the agent is about to write.
jakuta-contract preflight src/new_handler.rs

So now the agent is compiling against Rust's opinionated compiler, running our test suites, and checking that it obeys the Jakuta contract. The CLI can tell it where the blessed surface lives, why that surface exists, what changed in the shared contract, and whether the new code is bypassing a shared abstraction.

This is how the human starts getting out of the tedious loop. Instead of me asking, "Did you use the shared libraries properly? Did you bypass something the shared crates already own?" the agent can ask the contract CLI and get an answer before I ever see the PR.

Every crate's README markdown file is parsed into the CLI surface. The same idea applies here: make the wrong thing impossible and make the right thing the only thing. This principle protects against drift and lets us scale agents toward more autonomy, because the documentation, generated catalog, and CLI surface are forced to move together.

The general loop underneath all of this is the part I care about most.

Reasoning About Correctness by Construction in the AI Age

Before any of this works, you need a shift in thinking. Some companies and inherited codebases will make this harder than it should be. Fine. The prerequisites are:

• Assume the agent will not do anything it is not forced to do.
• Write code for agents and humans at the same time. Users touch the behavior. Developers maintain the system. Agents will be asked to edit it and will absolutely misuse whatever loose surface you leave lying around.

After that, every bug becomes evidence. The system allowed a bad shape to exist, and now you have to ask why.

Say an agent bypasses the response macro and hand-rolls a response type. The usual reaction is to add a check right there, or factor the repeated code into a reusable helper. That helps, but it is still too low. Ask why this bad shape was possible. What part of the API should be removed? What should become explicit instead of implicit? How far up the stack can we push the fix so this entire class of bugs disappears?

That gives us the actual loop:

• Find an issue.
• Ask why that issue was possible in the first place.
• Categorize it into the broader class of issues it belongs to.
• Refactor as far up the stack as you can to eliminate that class.
• Encode the rule in a hook so the agent cannot casually reintroduce it.
• Then ask what would make the hook fire less often in the first place.

After iterating on the hook, watch how agents try to weasel around it. If the same hook fires constantly, that is a hook smell. Sometimes the context injected by the hook is weak. Sometimes the skill or markdown file needs sharper wording. Often, in my experience, repeated hook fires mean I patched the code smell instead of the architectural reason the smell exists.

A good hook teaches you where the design is still leaking. If it fires all day, the codebase is still inviting the wrong move.

The answer lands at the right layer: hook, macro, crate, or even a language change.

AI has made these huge refactors newly realistic. In the past, a senior engineer or tech lead could say a large-scale correctness refactor was out of scope because it would take too long, and they were often right. Now the mechanical rewrite is no longer the blocker it used to be. You still need judgment and taste. You still need somebody who knows what the system is supposed to do.

Some of our style rules started as hooks. Perfect Rustacean and Perfect TypeScripter both follow the same idea: block the shape at write time, then move the rule deeper when the pattern keeps recurring. If agents keep trying a ternary-shaped collapse or a boolean-shaped state machine, the hook blocks it. If the pattern belongs in a macro, the macro eventually makes the hook quiet.

The CLI closes that loop. The agent can check itself, discover the right surface, read the rationale, and try again without waiting for a human to notice the same mistake.

"Gee Ozzy, it sounds like you almost don't trust the agent."

Quite the contrary. I trust the agent to be an agent.

AI Is Not Your Oracle

By this point, the argument should be clear: agents can do more than act like glorified Google or a desktop assistant. Give them the right tools, and they can do a lot more than autocomplete a function or summarize a file.

Agents get sold as cost-cutting machines. In fact, in some domains, doing this properly costs more up front, because asking the agent to type faster is the cheap part; the real work is building the tools, review paths, compute budget, and infrastructure that let the agent move quickly without lowering the standard of the codebase. The agent is only as useful as the environment you force it to work inside.

This pattern is older than AI. Every useful abstraction gets the same complaint at first: it is inefficient, it is a crutch, it is only for novices, real programmers will get worse if the tool does the work for them. The useful question is not whether the tool feels pure. It is what constraints make the tool reliable enough to use.

Some of the modern AI pushback is cope from older senior developers, and honestly, I sympathize with it. Imagine spending years memorizing syntax just for AI to memorize syntax better than you ever could.

But the moat to programming was never syntax. The moat has always been system design, reasoning about state, understanding the hardware, and knowing what goal you are actually trying to execute on.

Now, like it or not, understanding agents is becoming part of the craft. The job is to steer them, constrain them, and lead them directly toward the goal.

AI is not the oracle. You cannot be a serious programmer while strictly relying on AI. We heard a version of that story with SQL too. SQL was readable enough that people thought everyone would be able to program. Look around. That did not make software engineering disappear.

The useful posture is: assume the AI will miss things, then surround it with hooks, macros, CLIs, compiler errors, and tests that pull it back into shape.

Here is the public TypeScript side of that same idea. Perfect TypeScripter is one of the production plugins we use at Jakuta Inc. The public shape is enough to show the point:

• ban boolean collapse when the domain has more than two outcomes
• reject optional-field clusters that should be discriminated unions
• require exhaustiveness on discriminant switches
• block any, unsafe casts, and magic-string state where the domain wanted a real type
• install cross-file ESLint rules for duplicate envelope shapes, variant-literal drift, and phantom type parameters

Some of those are style notes. Some of them are hard correctness rules. All of them come from things we have seen agents and humans do in production code. Anyone can have an agent write a post about a nice idea. This is the stuff we actually make ourselves and our agents live under every day.

Every team has its own style and priorities, but ambiguity is not a personality trait. This is how I write code, and it is how I have seen strong developers cut down the back-and-forth that eats big projects alive. If the issues in this article feel familiar, or if Correctness by Construction clicked for you, try the rails. The payoff is not theoretical.

People complain about AI slop, and yes, there is a lot of it. We have all seen what it looks like in code by now. But let's not pretend slop code was invented by agents. Humans were writing plenty of it before the model showed up.

Throwing our hands up and saying AI agents are unusable, do not scale, or are not here to stay serves no one. The better move is to look at what is actually happening: agents are fast, agents are wrong sometimes, and the useful question is how much of that wrongness you can make unshippable.

The part you control is the system around the agent. Every time you catch a fresh class of mistake, move that lesson into the compiler, the hook, the macro, the CLI, or the test suite, so the next run has fewer ways to repeat it.

If you haven't yet, read Correctness by Construction for the ladder of techniques this piece assumes. The Dijkstra line from over there still applies: if programming is the process of putting bugs in, then the AI age just gave you a faster way to insert them, and equally fast machinery for refusing to let them stay.

Next in this series, still being written: Cognitive Complexity, Artificial Intelligence and Programming.