# Kavach Labs blog, in full Source: https://www.thekavachlabs.com/blog --- # What Invariants Should My Service Have? > This post is about state invariants, why developers find it hard to write them, and how we test if an invariant is actually doing its job. Koustav Chowdhury · Founder · October 19, 2026 · Guides 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](https://antithesis.com/blog/2026/agent_skills/)[†](https://github.com/kavachlabs/kavach/tree/main/skills) 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. ![From state-map.md to verified invariants in 61 microseconds. Without falsification, an agent writes a weak check that passes on the happy path and lets state corruption slip through. With /kavach-setup and /kavach-invariants, the agent writes .kavach/plan/state-map.md and invariants.md, injects a 1-line mutant for each invariant, verifies invariant_violated in 61.1 microseconds, and saves the kill table.](https://www.thekavachlabs.com/blog/what-invariants-should-my-service-have/d-plan-mutation-loop.diagram.svg "Checking every invariant against a planted bug in microseconds") 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](https://github.com/kavachlabs/kavach/tree/main/examples/ledger/.kavach/plan), 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. ```markdown # .kavach/plan/state-map.md — Wallet Ledger (examples/ledger) ## 1. Integration Mode - Mode: Direct Handler Instrumentation (Production kavach-recorder + kavach-host Replay) - Language & SDK: Go (github.com/kavachlabs/kavach/sdk/go) - Host Command (--bin): ./ledger ## 2. State Root & Mutable Structures | Structure / Field | Location (file:line) | Role & Consistency Requirement | | --- | --- | --- | | Ledger.Balances (map[string]int64) | sdk/ledger.go:40 | Primary per-account balance map; every account balance must remain >= 0. | | Ledger.Net (int64) | sdk/ledger.go:41 | Running net total of deposits - withdrawals; must always equal sum(Balances). | ``` **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. ```markdown # .kavach/plan/invariants.md — Wallet Ledger (examples/ledger) ### 1. balances_non_negative (Bounds & Non-Negativity) - State inspected: Ledger.Balances (sdk/ledger.go:114-121) - Law: For every account a in Ledger.Balances, l.Balances[a] >= 0 after every step. - Planned falsification mutant: sdk/ledger.go:68 — omit the l.Balances[ev.Account] < amount guard in withdraw so overdraft event evt-005 (seq 19) debits bob below zero. ### 2. money_conserved (Conservation Law) - State inspected: Ledger.Balances and Ledger.Net (sdk/ledger.go:122-131) - Law: sum(l.Balances) == l.Net after every step. - Planned falsification mutant: sdk/ledger.go:77 — skip the sender debit l.post(env, ev, ev.Account, -amount, at) during transfer so evt-003 (seq 9) credits bob without debiting alice. ## Falsification Results (Millisecond Mutation Sweep) | Invariant | 1-Line Mutant Injected (file:line) | Verdict | Replay Time | | --- | --- | --- | --- | | balances_non_negative | sdk/ledger.go:68: skip balance < amount on withdraw | invariant_violated(balances_non_negative)@19 | 61.1 µs | | money_conserved | sdk/ledger.go:77: skip sender debit on transfer | invariant_violated(money_conserved)@9 | 61.1 µs | ``` 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. ```bash curl -fsSL https://www.thekavachlabs.com/install.sh | sh npx skills add kavachlabs/kavach ``` ## References 1. [Antithesis skills for agents](https://antithesis.com/blog/2026/agent_skills/) (Article, antithesis.com) 2. [Kavach Agent Skills](https://github.com/kavachlabs/kavach/tree/main/skills) (Code, github.com) 3. [Wallet Ledger state-map.md and invariants.md](https://github.com/kavachlabs/kavach/tree/main/examples/ledger/.kavach/plan) (Docs, github.com) Source: https://www.thekavachlabs.com/blog/what-invariants-should-my-service-have --- # How to Read a Kavach Strip Chart > This post is a reference guide to the strip-chart diagrams on our site, showing how each lane, glyph, step line, and crash marker maps to a Kavach journal. Koustav Chowdhury · Founder · October 19, 2026 · Guides Before I introduce the strip charts on our blog, let me tell you who I am and where this started. I have worked in financial industry for about half-a-decade, and when I recently build HFT infrastructure from scratch, we had to read sequence timelines without getting lost in text logs. While building that, I found certain patterns that are helpful for me, and also helpful for agents, to debug faster, to reproduce the issue, and to verify the fixes. [A journal strip chart](https://github.com/kavachlabs/kavach/blob/main/SPEC.md)[†](https://github.com/kavachlabs/kavach/blob/main/journal/record.go) is about drawing the events which cause transitions in your state machine. What is a strip chart, you may ask? A strip chart is a software's visual tape which determines what inputs, reads, and outputs took place in each step. Why does a strip chart spark curiosity and help to debug a bug faster? Whenever we are stuck reproducing what happened by looking at the logs, the network packets, or different containers, a simple strip chart lays out in bare bones the events that took place, which caused the software to end up in the state that it did. 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 guess from a log line when you can inspect the tape. ![Anatomy of a Kavach Journal Strip Chart (SPEC.md §4–§6). Each vertical column is one sequence number (seq), dashed vertical lines mark handler step boundaries before every input (0x01), and the four horizontal lanes from top to bottom show input (0x01, solid tall block), clock (0x02, thin vertical pulse), rand (0x03, four staggered bit-ticks), and output (0x04, hollow square). At the far right, the yellow highlight band marks the failing step and the red line and block mark the crash marker (0x05).](https://www.thekavachlabs.com/blog/how-to-read-a-kavach-strip-chart/d-strip-chart-anatomy.diagram.svg "How to read every lane, glyph, step boundary, and marker on a Kavach journal tape") A Kavach strip chart is kind of like that. It has a transactional ledger which keeps account of all the state changes, all the state mutations that lead up to the crash. In a way, it makes the execution of an application auditable on every step. Now, since I have worked in the finance industry, I see its applications everywhere. It helps to reproduce bugs, to actually see what events preceded the crash happening, and so on. ```markdown # Reference Guide: Visual Elements of a Kavach Strip Chart (SPEC.md §4–§6) | Visual Element | Lane / Position | Record Type (`journal/record.go`) | SDK Call | Meaning & Replay Semantics (`SPEC.md §4–§6`) | | --- | --- | --- | --- | --- | | **Vertical grid column** | Left → right (`seq`) | Every `Record` (`u64 seq`) | — | One monotonically increasing sequence number (`seq`). Records appear in strict program order. | | **Dashed vertical line** | Full height | Before each `0x01` `input` | `Handle(env, in)` | **Step boundary.** Everything between two dashed lines happened inside one single-writer handler step. | | **Solid tall block (`■`)** | Lane 1 (Top) | `0x01` · `TypeInput` | `in kavach.Input` | **Upstream event.** Holds `source` (e.g. `"kafka:wallet-events"`), `position` (`"3:1042"`), and raw `data`. Served to start the step. | | **Thin vertical tick (`│`)** | Lane 2 | `0x02` · `TypeClock` | `env.Now()` | **Clock read.** Holds `unix_nanos` (`int64` UTC nanoseconds). Replay serves this exact timestamp back to the handler. | | **4 staggered bars (`'' ,,`)** | Lane 3 | `0x03` · `TypeRand` | `env.Read(buf)` | **Random read.** Holds raw entropy `data` bytes (e.g. an 8-byte transaction nonce). Replay serves the exact recorded bytes. | | **Hollow square (`□`)** | Lane 4 (Bottom) | `0x04` · `TypeOutput` | `env.Emit(sink, b)` | **Emitted side effect.** Drawn **hollow** because replay never executes outputs; it captures the handler's emission and compares it against this slot. | | **Yellow highlight band** | Last step | Last `input` → `marker` | — | **The failing step.** Highlights the entire step whose input triggered the failure (`SPEC.md §6`). | | **Red block + vertical line** | Top lane + full height | `0x05` · `TypeMarker` | Runtime / recorder | **Failure annotation.** Marks a `panic`, `error`, `invariant`, or `crash` that caused `kavach-recorder` to cut and flush the `.kavach` fixture. | ``` ```callout invariant | Why inputs, clocks, and random reads are solid ink, while outputs are hollow squares Look closely at the four lanes on the tape. The top three lanes—`input` (`0x01`), `clock` (`0x02`), and `rand` (`0x03`)—are drawn as **solid filled shapes**. The fourth lane—`output` (`0x04`)—is drawn as an **unfilled hollow outline**. That visual contrast encodes the core law of deterministic replay (`SPEC.md §6`): - **Filled marks are inputs and reads fed *into* the handler.** During replay, `kavach-host` serves the recorded `input` to start the step, and whenever the handler calls `env.Now()` or `env.Read()`, `kavach-host` pops the next solid mark in order and hands those exact bytes back. - **Hollow squares are expectations to be *verified*.** During replay, outputs are never delivered to Kafka or Postgres. Instead, each hollow square is an empty frame waiting to be compared byte-for-byte against what the replayed handler emits. ``` ## Why the shapes inside a step matter Starting from a snapshot, if you keep reading the events that are in the journal, each column shows what happened in that step. That's the ultimate goal for [our reference diagram](https://github.com/kavachlabs/kavach/blob/main/examples/ledger/sdk/ledger.go)[†](https://github.com/kavachlabs/kavach/blob/main/examples/ledger/testdata/null-amount.kavach). What makes it interesting are the shapes sprinkled across the lanes. A solid block comes from an input. A thin tick can come from the clock. Four bars can come from the fact that we are reading random bytes before emitting a hollow box. Having the ability to read deterministically what happened in production from these four lanes is one of the key guarantees of our journal format, and that is what makes the diagram so useful. ```go func (l *Ledger) Handle(env kavach.Env, in kavach.Input) error { var ev Event if err := json.Unmarshal(in.Data, &ev); err != nil { return fmt.Errorf("decode event at %s: %w", in.Position, err) } amount := *ev.Amount // [!code error] if amount <= 0 { return reject(env, ev, "amount must be positive") // [!code highlight] } at := env.Now() // records 'clock' (0x02) in Lane 2 switch ev.Type { case "deposit": l.Net += amount return l.post(env, ev, ev.Account, amount, at) // 1x (rand + output) case "transfer": if l.Balances[ev.Account] < amount { return reject(env, ev, "insufficient funds") // clock + output (no rand) } if err := l.post(env, ev, ev.Account, -amount, at); err != nil { return err } return l.post(env, ev.To, amount, at) // 2x (rand + output) } return nil } ``` ## Challenges of reading production traces These challenges all come down to seeing what happened inside a step. Reading a production trace has several such traps. **Two-leg transfers and single deposits.** Can a text log show everything? Show every branch? How does it know when a step is a transfer? Which helper ran twice? If these reads aren't drawn on the tape, the same transfer looks just like a deposit in the logs. As a company, Kavach Labs is going to tackle these challenges so that any trace is easy to read. **Early rejections and silent steps.** Software often checks inputs in more than one place. Say you design a service that rejects a bad amount before reading the clock. How do you see that without stepping through a debugger? With 1,000 requests it may look fine, but on an early rejection you are skipping the clock and random reads altogether. **The yellow band and red crash marker.** One system requirement for a crash fixture is that your failing step should stand out right away. Most single-threaded deterministic software follows this step order, but quite a few log viewers still don't. How do you model those? These are the uncomfortable parts of the system that we want to tackle. ```markdown # Step-by-Step Decoding of the 35-Record Strip Chart in the Picture | Step | Columns (`seq`) | Records in Step (`0x01`–`0x05`) | Cols | What Happened in the Handler | | --- | --- | --- | --- | --- | | **Step 1** | `seq 0..5` | `input` → `clock` → `rand` → `output` → `rand` → `output` | 6 | Two-leg operation (e.g. `transfer`): 1 clock read, 2 nonce reads + 2 emitted entries. | | **Step 2** | `seq 6..9` | `input` → `clock` → `rand` → `output` | 4 | Single-leg operation (e.g. `deposit` or `withdraw`): 1 clock read, 1 nonce read, 1 output. | | **Step 3** | `seq 10..11` | `input` → `output` | 2 | Fast validation rejection emitted before `env.Now()` or `env.Read()`. | | **Step 4** | `seq 12..15` | `input` → `clock` → `rand` → `output` | 4 | Single-leg operation: 1 clock read, 1 nonce read, 1 output. | | **Step 5** | `seq 16..17` | `input` → `clock` | 2 | Silent no-op step: read the clock, emitted no output. | | **Step 6** | `seq 18..22` | `input` → `rand` → `output` → `rand` → `output` | 5 | Clockless two-emission step: 2 random reads and 2 outputs without calling `env.Now()`. | | **Step 7** | `seq 23..28` | `input` → `clock` → `rand` → `output` → `rand` → `output` | 6 | Two-leg operation: 1 clock read, 2 nonce reads + 2 emitted entries. | | **Step 8** | `seq 29..32` | `input` → `clock` → `rand` → `output` | 4 | Single-leg operation: 1 clock read, 1 nonce read, 1 output. | | **Step 9** | `seq 33..34` | `input` → `marker` (shaded yellow + red line) | 2 | **Failing step:** panics immediately after `input` before reaching `env.Now()`. | ``` ```callout note | What about the other four record types in SPEC.md §4? The strip chart plots the four per-step high-frequency lanes (`0x01` `input`, `0x02` `clock`, `0x03` `rand`, `0x04` `output`) plus `0x05` `marker`. A full `.kavach` journal (`SPEC.md §4.6–§4.9`, `journal/record.go`) also defines four structural and boundary record types: - `0x06` `snapshot`: The handler's serialized state at the start of a segment (`start: "snapshot"`). - `0x07` `gateway`: An external query (`request`, `response`, `error`, `scope`) served back during replay without calling the network. - `0x08` `environment`: Process `env.*` variables (secrets hashed with SHA-256), `flag.*` evaluations, and `host.*` / kernel facts recorded at genesis (`seq 0`) and on drift between steps. - `0x09` `config`: Dynamic feature flag or limit reads made by the handler inside a step via `Env`. ``` ```interactive /interactive/replay-lab.html?scene=crash Click any mark on the 33-record null-amount.kavach strip chart below to inspect its sequence number, record type, JSON payload, and live account balances. ``` 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 read a journal tape, replay the crash, fix the code, and deploy the fix with more confidence. ## References 1. [Kavach Journal Format Specification (v0, §3–§6)](https://github.com/kavachlabs/kavach/blob/main/SPEC.md) (Spec, github.com) 2. [journal/record.go — Record Type Codes and Payload Framing](https://github.com/kavachlabs/kavach/blob/main/journal/record.go) (Code, github.com) 3. [examples/ledger/sdk/ledger.go — Single-Writer Wallet Handler](https://github.com/kavachlabs/kavach/blob/main/examples/ledger/sdk/ledger.go) (Code, github.com) 4. [null-amount.kavach — 34-Record Crash Fixture](https://github.com/kavachlabs/kavach/blob/main/examples/ledger/testdata/null-amount.kavach) (Code, github.com) Source: https://www.thekavachlabs.com/blog/how-to-read-a-kavach-strip-chart --- # The Hidden Tests Pass. The Contract Doesn't. > This post is about why unit tests miss regressions when coding agents build new features, and how contract-first verification catches them before code review. Koustav Chowdhury · Founder · October 18, 2026 · Product Before I introduce feature contracts, let me tell you who I am and why we built this. I have worked in financial industry for about half-a-decade, and when I recently build HFT infrastructure from scratch, we never shipped a new order type without replaying recorded traffic against it first. 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. [Contract verification](https://antithesis.com/blog/2026/declarative_testing/)[†](https://antithesis.com/blog/testing_pyramid/) is about locking the traffic and invariants which govern transitions in your state machine. What is a behaviour contract, you may ask? A behaviour contract is a software's locked baseline which determines whether old traffic stays untouched and new feature traffic obeys the rules. Why does a behaviour contract help to catch regressions faster? Whenever we are stuck reviewing a feature pull request by looking at unit tests that the agent wrote itself, a simple contract check lays out in bare bones the events that took place, which caused the software to change its output. 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 green unit test when a new fee rule silently changed existing balances. ![Contract-first feature verification (/kavach-implement). Step 1: Contract Init combines traffic.kavach and spec invariants, verifying unreached@N on the old build. Step 2: Human Approval via kavach contract approve locks the SHA-256 of traffic and invariants. Step 3: The Agent Loop runs kavach_contract_check across non-feature and feature step variants, rejecting builds with regression@N, invariant_violated(X)@N, variant_failed(K)@N, or stale_lock until verdict: pass.](https://www.thekavachlabs.com/blog/the-hidden-tests-pass-the-contract-doesnt/d-contract-verification.diagram.svg "Contract-first verification locks baseline traffic and spec invariants before the agent writes feature code") A feature contract is kind of like that. It has a transactional ledger which keeps account of all the state changes, all the state mutations that lead up to the new feature's output. In a way, it makes the impact of a new feature auditable. Now, since I have worked in the finance industry, I see its applications everywhere. It helps to catch silent regressions, to actually see what existing events changed their output, and so on. ```bash kavach contract init \ --spec SPEC.md \ --traffic traffic.kavach \ --feature-match '$.argv[0]=="NEWCMD"' \ --invariant capacity_non_negative \ --invariant-source handler.go kavach contract check --old /tmp/old --new /tmp/old ``` ```callout invariant | Why kavach mcp has no tool for 'contract approve' Look at the five MCP tools in `kavach mcp`: `kavach_list_incidents`, `kavach_replay`, `kavach_diff`, `kavach_contract_show`, and `kavach_contract_check`. There is deliberately **no `kavach_contract_approve` tool**. Approving a contract writes a cryptographic lock over the recorded traffic, the feature step selectors, and the source code of the declared invariants. If an agent edits an invariant or tampers with the contract during implementation, `kavach_contract_check` immediately fails with `stale_lock`. An agent can never grade its own homework. ``` ## Why locking the contract matters Starting from a snapshot, if you keep replaying the events that are in the journal, old steps should match the old build and new steps should satisfy the invariants. That's the ultimate goal for [contract verification](https://benchmark.kavachlabs.dev)[†](https://github.com/kavachlabs/kavach/blob/main/SPEC.md). What makes it challenging are certain habits sprinkled through coding agents. Regressions come from shared helpers. They can come from weakened checks. They can come from the fact that the agent is editing the test to make it pass. Having a human approve and lock the contract before the agent writes the code is one of the key guarantees of our workflow, and that is what makes the verification trustworthy. ```markdown # Contract Verification Requirements (SPEC.md §6.4) | Step Class | Requirement on New Build | Verdict on Failure | | - | - | - | | Non-feature steps | Must produce byte-identical outputs to Old Build | regression@N | | Feature steps | Must change from Old Build (proving feature is wired in) | unreached@N | | All steps | Every declared spec invariant must hold after every step | invariant_violated(X)@N | | Feature variants | Perturbed variants of feature steps must not fail | variant_failed(K)@N | ``` ```callout deep-dive | Stopping runaway agent loops: round and streak tracking When an agent gets stuck on a subtle invariant violation, left to itself it will burn tokens in an infinite edit-test loop or try to delete the failing check. `kavach contract check` tracks both `round` and `streak` (how many consecutive checks produced the exact same failure). Per `AGENTS.md`, when `streak` reaches 3—or `round` reaches 8—the agent must stop immediately and report the exact failing step and invariant to the human operator. ``` ## Challenges of evaluating coding agents on features These challenges all come down to what happens outside the happy path. Evaluating an agent's feature has several such traps. **Silent regressions on existing traffic.** Can a unit test suite catch everything? Catch every changed byte? How does it know what the old output was on a thousand earlier requests? Which helper function did the agent touch? If these old requests aren't replayed, the same events can produce different outputs in production. As a company, Kavach Labs is going to tackle these challenges so that any regression on existing traffic is caught right away. **Agents editing the checks.** Software often keeps tests and implementation in the same repository. Say you ask an agent to implement a feature that fails an invariant check. How do you verify the code if the agent can edit the invariant file itself? With 1,000 lines of diff it may look fine, but in the middle the agent weakened the rule to make the test pass. **Edge cases that happy-path tests miss.** One system requirement for feature verification is that your invariants should hold across variations of the new command. Most careful engineers test these edge cases, but quite a few chunks of agent code still don't. How do you model those? These are the uncomfortable parts of the system that we want to tackle. We're building Kavach Labs to tackle this problem head-on. We love contract verification as an architectural concept, and we want agentic software to be written and deployed so that it's easy to lock a contract, replay it, fix the code, and deploy the feature with more confidence. ## References 1. [A declarative restoration](https://antithesis.com/blog/2026/declarative_testing/) (Article, antithesis.com) 2. [The Testing Pyramid is upside-down](https://antithesis.com/blog/testing_pyramid/) (Article, antithesis.com) 3. [Kavach Bench: Multi-Arm Coding Agent Evaluation Console](https://benchmark.kavachlabs.dev) (Code, benchmark.kavachlabs.dev) 4. [Kavach Specification §6.4: Feature Steps and Contracts](https://github.com/kavachlabs/kavach/blob/main/SPEC.md) (Spec, github.com) Source: https://www.thekavachlabs.com/blog/the-hidden-tests-pass-the-contract-doesnt --- # Why Coding Agents Write Narrow Fixes (And Why Logs Won't Save Them) > This post is about why coding agents write narrow patches that only fix one crash trace, and how replaying 56 variants catches those patches in milliseconds. Koustav Chowdhury · Founder · October 16, 2026 · Engineering Before I introduce variant verification, let me tell you who I am and why we built this. I have worked in financial industry for about half-a-decade, and when I recently build HFT infrastructure from scratch, we never merged a bug fix without replaying recorded traffic variations against it first. 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. [Variant verification](https://antithesis.com/blog/2026/time-traveling-agents/)[†](https://antithesis.com/blog/2025/findability/) is about replaying the event variations which govern transitions in your state machine. What is a narrow fix, you may ask? A narrow fix is a software's incomplete patch which determines whether only the recorded crash passes while sibling events still fail. Why does a variant check help to catch narrow fixes faster? Whenever we are stuck reviewing a bug fix pull request by looking at unit tests that the agent wrote itself, a simple variant check lays out in bare bones the events that took place, which caused the software to fail on sibling inputs. 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 green unit test when a deposit patch still leaves transfers broken. ```json {"id": "evt-008", "type": "deposit", "account": "bob", "amount": null} ``` ```go if event.Type == "deposit" && event.Amount == nil { env.Emit("ledger.rejections", Rejection{Event: event.ID, Reason: "missing amount"}) return nil } ``` ![Why single-trace reproduction lets coding agents ship narrow fixes. The top lane shows that without variant verification, an Incident at seq 31 (deposit: amount=null) leads the agent to write a narrow guard (if type=="deposit" && nil), which merges and crashes in production tomorrow on transfer: amount=null. The bottom lane shows kavach mcp running 56 incident perturbations and 48 neighbour regressions in 5.9 ms, rejecting the narrow patch with variant_failed(6)@22 (deposit to transfer), forcing the agent to guard all events until verdict: fixed (47/47 variants pass).](https://www.thekavachlabs.com/blog/why-coding-agents-write-narrow-fixes/d-agent-verdict-loop.diagram.svg "Single-trace reproduction rewards narrow patches; variant perturbation rejects them") A variant verifier is kind of like that. It has a transactional ledger which keeps account of all the state changes, all the event variations that lead up to the same crash. In a way, it makes the generality of a bug fix auditable. Now, since I have worked in the finance industry, I see its applications everywhere. It helps to catch narrow patches, to actually see what variations break the fix, and so on. ```callout invariant | What counts as a verified fix in Kavach (SPEC.md §6.1) A candidate build only receives the verdict `fixed` when: 1. The recorded failure is gone and all declared invariants hold after every step. 2. Every step *before* the failing input produces the exact outputs production saw (no collateral behaviour changes). 3. The build passes at least 10 **reproducing incident variants**—perturbed copies of the journal on which the old build still fails the same way. 4. The build matches the old build's outputs across up to 48 **neighbour regression variants**—mutations of earlier valid inputs that resemble the failing one. ``` ```interactive /interactive/replay-lab.html?scene=variants Interactive fix verification across the ledger crash variants: toggle between the narrow deposit-only patch and the general patch. ``` ## Why deterministic variants matter Starting from a snapshot, if you keep replaying the variations that are in the journal, your fix should hold on every step. That's the ultimate goal for [Kavach](https://github.com/kavachlabs/kavach/blob/main/AGENTS.md)[†](https://github.com/kavachlabs/kavach/blob/main/BENCHMARKS.md). What makes it challenging are certain shortcuts sprinkled through agent patches. Shortcuts come from hardcoding an event ID. They can come from guarding only one branch. They can come from the fact that the agent is rejecting valid inputs too. Having the ability to replay 56 variations deterministically in milliseconds is one of the key guarantees of our verifier, and that is what makes the agent loop so reliable. ```callout spike-pit | Why incident variants alone aren't enough: the "drop everything" cheat What if an agent fixes a crash by rejecting *every* deposit—valid or invalid? Every incident variant will stop crashing! That is why `kavach diff` also generates up to 48 **regression variants** (`--regressions 48`): it takes earlier inputs in the journal that succeeded on the old build and resemble the failing input, perturbs them, and verifies that `--new` produces the exact same outputs as `--old`. If an over-broad fix breaks valid traffic, `kavach diff` rejects it with `regressed(K)@N`. ``` ## Challenges of verifying agent bug fixes These challenges all come down to how agents optimize for a passing test. Verifying an agent's patch has several such traps. **Guarding only one branch.** Can a single replay catch a narrow patch? Catch every missing guard? How does it know what happens on a transfer? Which other branches share the same bug? If these variations aren't tested, the same bug will crash production the next day on a different event type. As a company, Kavach Labs is going to tackle these challenges so that narrow fixes get rejected automatically. ```markdown # Ten Planted Bugs Benchmark (bench/bugs.go) — go test ./bench -run TestBenchmark -v | # | Planted Bug | Tempting Narrow Fix | Verdict | | - | - | - | - | | 1 | Nil pointer on missing email | Guard signup only, leave profile_update unguarded | variant_failed | | 2 | Slice index on empty items | Guard checkout only, leave quote unguarded | variant_failed | | 3 | Division by zero on metric window | Guard only the recorded metric name | variant_failed | | 4 | Write to uninitialized nil map | Init map only when step 0 is init | variant_failed | | 5 | Type assertion panic on string qty | Validate qty type but forget price | variant_failed | | 6 | Group booking exceeds capacity | Check capacity on reserve but not extend | variant_failed | | 7 | Update delivered before create | Buffer only for the recorded customer ID | variant_failed | | 8 | Redelivered charge applied twice | Deduplicate only back-to-back duplicates | variant_failed | | 9 | Leap-day array index on day 366 | Special-case the exact recorded timestamp | variant_failed | | 10 | Modulo zero on empty lottery pool | Refill pool only at the recorded draw count | variant_failed | ``` **Variations that don't reproduce the bug.** Software often behaves differently when you change a field value. Say you design a check that replaces a missing amount with 5,000 dollars. How do you score that test without running it on the old build first? With 5,000 dollars the old build works fine, so on replay you are testing a happy path and not the crash. **Patches that break valid traffic.** One system requirement for a good fix is that earlier valid events should produce the exact same outputs as before. Most careful human patches follow this principle, but quite a few chunks of agent code still don't. How do you catch those? These are the uncomfortable parts of the system that we want to tackle. ```bash claude mcp add kavach -- kavach mcp npx skills add kavachlabs/kavach ``` 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 capture a bug, replay it, fix the code, and deploy the fix with more confidence. ## References 1. [Your agent can now ship reliable distributed systems](https://antithesis.com/blog/2026/time-traveling-agents/) (Article, antithesis.com) 2. [Did you get lucky or unlucky?](https://antithesis.com/blog/2025/findability/) (Article, antithesis.com) 3. [Kavach Agent Loop & Verdict Specification (AGENTS.md)](https://github.com/kavachlabs/kavach/blob/main/AGENTS.md) (Docs, github.com) 4. [Kavach Ten Planted Bugs Benchmark](https://github.com/kavachlabs/kavach/blob/main/BENCHMARKS.md) (Code, github.com) Source: https://www.thekavachlabs.com/blog/why-coding-agents-write-narrow-fixes --- # 81.2 Nanoseconds: Designing an Always-On Production Flight Recorder > This post is about where the determinism boundary should live in a backend service, and how our shared-memory ring buffer records every event in 81.2 nanoseconds. Koustav Chowdhury · Founder · October 14, 2026 · Engineering Before I introduce our flight recorder, let me tell you who I am and where this started. I have worked in financial industry for about half-a-decade, and when I recently build HFT infrastructure from scratch, we had to record live traffic without slowing down the hot path. 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. [Flight recording](https://antithesis.com/blog/deterministic_hypervisor/)[†](https://antithesis.com/blog/2026/retrologging/) is about journaling the inputs which cause transitions in your service handler. What is a determinism boundary, you may ask? A determinism boundary is a software's internal line which determines what events get captured for offline replay. Why does a lightweight boundary help to debug a bug faster? Whenever we are stuck reproducing what might have happened by looking at the logs, the network packets, or different containers, a simple handler boundary lays out in bare bones the events that took place, which caused the software to end up in the state that it did. 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 guess from a test lab when your live balance is wrong. ![Where should the determinism boundary live? The top lane shows a Full-VM Hypervisor Boundary using x86 instruction-retired PMC and a Guest OS pinned to 1 core per VM, passing through a Container Topology of Broker, DB, and Mocks, where adding a printf causes a Timing Butterfly Effect with no local ARM64 support. The bottom lane shows the Kavach Handler Boundary (SPEC.md §10.7) where a Service Handler Step reads env.Now(), env.Read(), and env.Emit() across an 8 MiB Shared Ring at 81.2 ns per event with 0 syscalls, drained by kavach-recorder into a 1,954-byte .kavach fixture that replays in 61.1 microseconds.](https://www.thekavachlabs.com/blog/81-nanoseconds-in-process-flight-recorder/d-ring-boundary.diagram.svg "Determinizing at the handler environment boundary avoids the x86 instruction-counter butterfly effect") An in-process flight recorder is kind of like that. It has a transactional ledger which keeps account of all the state changes, all the state mutations that lead up to the crash. In a way, it makes the execution of an application auditable on every step. Now, since I have worked in the finance industry, I see its applications everywhere. It helps to reproduce bugs, to actually see what events preceded the crash happening, and so on. ```callout spike-pit | Why syscall recording (rr) isn't free in production either Tools like Mozilla's `rr` move the boundary up from the hypervisor to Linux kernel syscalls and `perf` counters. That works well for local C++ debugging, but `ptrace` traps, `seccomp` filters, and single-threaded serialization add 1.2x to 2x runtime overhead—far too heavy to leave running inside a live payment ledger or order gateway. ``` ```go func (l *Ledger) Handle(env kavach.Env, in kavach.Input) error { now := env.Now() // recorded as a 'clock' frame var nonce [8]byte _, _ = env.Read(nonce[:]) // recorded as a 'rand' frame entry, err := l.apply(in.Data, now, nonce) if err != nil { return err } env.Emit("ledger.entries", entry) // recorded as an 'output' frame return nil } ``` ## Why shared memory matters for recording Starting from a snapshot, if you keep replaying the events that are in the journal, you should end up with the exact crash state. That's the ultimate goal for a flight recorder. What makes it challenging are certain bits of overhead sprinkled through the operating system. Overhead comes from the kernel. It can come from system calls. It can come from the fact that we are copying bytes over a pipe on every event. Having the ability to record deterministically in shared memory in about eighty nanoseconds is one of the key guarantees of [Kavach](https://github.com/kavachlabs/kavach/blob/main/SPEC.md)[†](https://github.com/kavachlabs/kavach/blob/main/BENCHMARKS.md), and that is what makes always-on recording possible in production. ```bash go test -run '^$' -bench RecorderStep -benchtime 2s -count 5 ./replay ``` ```callout deep-dive | What the 81.2 ns/event benchmark includes (and doesn't) The benchmark runs a sustained stream that fills the 8 MiB ring within milliseconds, so the 81.2 ns/event median includes any backpressure wait for `kavach-recorder` to drain, number, and compress frames on another core. It injects a seeded `math/rand` source rather than `crypto/rand` so the benchmark measures Kavach's ring and framing overhead rather than the kernel's CSPRNG. ``` ## Challenges of recording live production services These challenges all come down to recording without slowing down the service. Production recording has several such traps. **Losing the last event on a crash.** Can a flight recorder capture everything? Capture every panic? How does it know what the input was when the process died? Which step was the handler running? If these events aren't in shared memory, a crash wipes out the very input you needed to see. As a company, Kavach Labs is going to tackle these challenges so that the shared ring keeps the last input safe on disk. **Slowing down the hot path.** Software often writes logs or traces in more than one place. Say you design a service that writes every step over a pipe. How do you record without paying for a system call on every event? With 1,000 requests a second it may behave fine, but under a traffic spike you are blocking the handler on the kernel. **Replaying without external services.** One system requirement for fast replayability is that your handler should read its clock and inputs from the journal. Most single-threaded deterministic software follows this principle, but quite a few chunks of software still don't. How do you model those? These are the uncomfortable parts of the system that we want to tackle. ```interactive /interactive/replay-lab.html?scene=crash The 33-record ledger crash fixture: scrub through the recording to inspect inputs, clock reads, random reads, and outputs. ``` We're building Kavach Labs to tackle this problem head-on. We love deterministic recording as an architectural concept, and we want agentic software to be written and deployed so that it's easy to capture a bug, replay it, fix the code, and deploy the fix with more confidence. ## References 1. [So you think you want to write a deterministic hypervisor?](https://antithesis.com/blog/deterministic_hypervisor/) (Article, antithesis.com) 2. [Free log storage with a time machine](https://antithesis.com/blog/2026/retrologging/) (Article, antithesis.com) 3. [Kavach Journal and Protocol Specification (v0)](https://github.com/kavachlabs/kavach/blob/main/SPEC.md) (Spec, github.com) 4. [Kavach Reproducible Benchmarks](https://github.com/kavachlabs/kavach/blob/main/BENCHMARKS.md) (Code, github.com) Source: https://www.thekavachlabs.com/blog/81-nanoseconds-in-process-flight-recorder --- # Event Sourcing > This post is about event sourcing and why the fundamentals of event sourcing matter in this age of agentic software. Koustav Chowdhury · Founder · October 7, 2026 · Concepts Before I introduce event sourcing, let me tell you who I am. I have worked in financial industry for about half-a-decade, and I recently build HFT infrastructure from scratch. 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. [Event sourcing](https://martinfowler.com/eaaDev/EventSourcing.html)[†](https://www.classcentral.com/course/youtube-event-sourcing-martin-fowler-yow-2016-193517)[†](https://gist.github.com/xpepper/36beda855540b0c1dde6c4c417dafec9) is about journaling the events which cause transitions in your state machine. What is a state machine, you may ask? A state machine is a software's internal status which determines the next business outcome. Why does event sourcing help to debug a bug faster? Event sourcing is an architectural decision which allows you to replay the software's path in an offline manner. Whenever we are stuck reproducing what might have happened by looking at the logs, the network packets, or different microservices, a simple event sourcing system lays out in bare bones the events that took place, which caused the software to end up in the state that it did. The bug reproduction becomes very fast, and that is one of the ideal goals of an event-sourced system. ![Events cause transitions in a state machine, which determines the next business outcome. Events are also written to an event journal, which lays out the events for an offline replay of the software's path, leading to very fast bug reproduction. Separately, debugging from logs, network packets and microservices leaves a developer stuck reproducing what happened.](https://www.thekavachlabs.com/blog/event-sourcing/d-muz6gsb9.diagram.svg "Event journal replay speeds bug reproduction compared with reading logs") ## Why event logs matter So let me explain it a bit more clearly: what exactly is an event source system, and where have we been seeing one in practice? 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 to spend 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 the bank's website pixels displaying that you have 10 dollars. ![Credits and debits flow into the transaction ledger, which is highlighted as the source. An arrow labelled summation takes the ledger to the bank account balance, and the balance flows to the website. The website displays 10 dollars, marked as failure, while last night's check of 100k doesn't match it. A final arrow labelled demand ledger points from the website back to the transaction ledger.](https://www.thekavachlabs.com/blog/event-sourcing/d-muz972ez.diagram.svg "Bank balance is derived from the transaction ledger, not stored directly") An event source system is kind of like that. It has a transactional ledger which keeps account of all the state changes, all the state mutations that lead up to your current state. In a way, it makes the state of an application auditable. Now, since I have worked in the finance industry, I see its applications everywhere. It helps to reproduce bugs, to actually see what events preceded the bug happening, and so on. ## Why deterministic replay matters Starting from a snapshot, if you keep replaying the events that are in the journal, you should end up with the current state. That's the ultimate goal for an event-sourced system. What makes it challenging are certain bits of non-determinism sprinkled through software. Non-determinism comes from the kernel. It can come from network jitter. It can come from the fact that we are not modeling our events properly. Having the ability to replay deterministically what changes to the state happened in production is one of the key guarantees of an event-sourced system, and that is what makes the paradigm so powerful. ## Challenges of replaying event logs These challenges all come down to non-determinism. Event sourcing has several such sources. **Hidden inputs.** Can an event-sourced system replay everything? Replay every bug? How does it know what the environment variables were? Which feature flags was the software using? If these aren't captured, the same events can produce different behavior on replay. As a company, Kavach Labs is going to tackle these challenges so that replay becomes truly deterministic. ![Hidden inputs in event-sourced replay. Same events are replayed into a Replay box. Environment variables and feature flags each point into Replay with a 'captured?' arrow. From Replay, 'not captured' leads to Different behavior, marked as failing, and 'captured' leads to Truly deterministic replay, which is highlighted.](https://www.thekavachlabs.com/blog/event-sourcing/d-muze2oh9.diagram.svg "Uncaptured environment variables and feature flags break deterministic replay") **Multiple views and replicated state.** Software often keeps state in more than one place. Say you design an event store that writes to an in-memory database. How do you replay without knowing the state of that database? With 1,000 rows it may behave one way, but on replay you are working with a fresh database clone. **State that isn't derived from the journal.** One system requirement for replayability is that your state should be a first-order derivative of the journal. Most single-threaded deterministic software follows this principle, but quite a few chunks of software still don't. How do you model those? These are the uncomfortable parts of the system that we want to tackle. ![The event store commits to the highlighted Journal, which feeds two targets: an arrow labelled replicate leads to the in-memory database with rows 1 to 1,000, and an arrow labelled replay leads to a fresh database clone. A separate failing box, labelled State not derived from the journal, has no arrows connecting it to the rest of the diagram.](https://www.thekavachlabs.com/blog/event-sourcing/d-muze4qf0.diagram.svg "Event store commits to a journal that feeds replicated database state") We're building Kavach Labs to tackle this problem head-on. We love event sourcing as an architectural concept, and we want agentic software to be written and deployed so that it's easy to capture a bug, replay it, fix the code, and deploy the fix with more confidence. ## References 1. [Event Sourcing](https://martinfowler.com/eaaDev/EventSourcing.html) (Article, martinfowler.com) 2. [Event Sourcing - Martin Fowler (YOW! 2016)](https://www.classcentral.com/course/youtube-event-sourcing-martin-fowler-yow-2016-193517) (Video, classcentral.com) 3. [My notes on the talk "The Many Meanings of Event-Driven Architecture" by Martin Fowler (GOTO 2017)](https://gist.github.com/xpepper/36beda855540b0c1dde6c4c417dafec9) (Article, gist.github.com) Source: https://www.thekavachlabs.com/blog/event-sourcing