What Invariants Should My Service Have?

Before I get into invariants, let me tell you why this question keeps coming up. I have worked in financial industry for about half-a-decade, and when I recently build HFT infrastructure from scratch, we had to check our state after every single event. While building that, I found certain patterns that are helpful for me, and also helpful for agents, to debug faster, to reproduce the issue exactly, and to verify the fixes.

An invariant¹² is about checking the laws of your state machine after each transition. What is a state invariant, you may ask? A state invariant is a software's internal rule which determines whether the business state is still valid after an event takes place.

Why does an invariant help to catch a bug faster? Whenever we are stuck wondering if a code change broke something subtle, a good invariant lays out in bare bones what must always remain true in the state. Most of us grew up writing unit tests. Let's say you have a bank account. Your bank account is a summation of all the credits and debits of your money. Now imagine one day you go up to your bank, and it says that you have 10 dollars. When you checked last night, you had 100k. So you will demand the transaction ledger for this, right? You are not ready to accept a single unit test saying one deposit function worked.

A state invariant is kind of like that. It checks the transactional ledger after every state change, every state mutation that leads up to your current balance. In a way, it makes the correctness of an application auditable on every step.

Now, since I have worked in the finance industry, I see its applications everywhere. It helps to catch bad state transitions, to see which exact event broke the accounting, and so on.

Why deterministic replay matters for invariants#

Starting from a snapshot, if you keep replaying the events that are in the journal, your invariants should hold on every step up to the current state. That's the ultimate goal when you are verifying a service. What makes it challenging is that most people don't know which invariants to write first, or how to check if their invariants are actually working.

Having the ability to replay deterministically what happened in production, and to check your invariants in microseconds, is one of the key guarantees of Kavach³, and that is what makes this workflow so useful for coding agents.

Challenges of writing invariants with agents#

These challenges all come down to how agents test their own work. Writing invariants with an agent has several such traps.

Checks that do nothing. Can an agent tell if an invariant is actually good? Test every edge case? How does it know if the check is doing anything at all? If an invariant function just returns true without checking the state, the same 1,000 events in the journal will pass on replay. As a company, Kavach Labs is tackling this by forcing the agent to break the code and prove the invariant catches the bug.

State kept in multiple places. Software often keeps state in more than one map. Say you design a wallet service that keeps account balances in one map and net deposits in another variable. How does the agent know how they relate without a map of the state? With 1,000 events it may look fine, but on a transfer bug the two numbers drift apart. So our setup skill writes a state map file in the repo first, before touching the code.

Invariants that aren't falsified. One requirement for trusting an invariant is that a broken build should make it fail. Most teams never test their assertions against broken builds because container simulations take half an hour, so quite a few chunks of software have weak checks. How do you test those fast? In Kavach, replay runs in 61 microseconds in memory, so our invariant skill injects a one-line bug, replays the journal, and checks that the invariant fails. These are the uncomfortable parts of verification that we want to tackle.

We're building Kavach Labs to tackle this problem head-on. We love deterministic verification as an architectural concept, and we want agentic software to be written and deployed so that it's easy to map your state, falsify your invariants, fix the code, and deploy with more confidence.

curl -fsSL https://www.thekavachlabs.com/install.sh | sh
npx skills add kavachlabs/kavach