# Formal methods can start small > Source: > Published: 2026-09-23 00:43:38+00:00 We have been curious about provable code for most of our working lives: the idea that a program could be shown correct rather than merely tested. [Knuth's line](https://www-cs-faculty.stanford.edu/~knuth/faq.html) has stayed with us as both a joke and a warning: "Beware of bugs in the above code; I have only proved it correct, not tried it." Some years ago, friends of ours tried to start a company around these methods for commercial software. The mathematics was the easy part. But before the tools could say anything about an existing codebase, someone had to describe it precisely enough. That someone was an engineer who was needed elsewhere, working for months with nothing to show for it. We looked at this from the outside, and decided it was imponderable. The objection is still current. Under [an earlier article of Valentyn's](https://www.yovico.ai/blog/the-equation-and-ai/) about formal specification, a reader on LinkedIn joked that the only downside is having to enter two million words to produce a two-input NAND gate, and asked how much writing the next generation of CPUs and GPUs would require. Proof assistants are usually introduced through their hardest applications: difficult theorems, verified compilers, intricate algorithms. Reading those, you get the impression that opening one means signing up for a large mathematical project. However, you don't need quantum mechanics to keep a household budget, and you don't need it here either. Agda, Rocq (formerly Coq), and Lean have the same range: detailed correctness arguments for complicated algorithms at one end, a few product states with what is allowed in each at the other. Since then, two things happened that make the objection weaker. A specification can be made executable and used as a test oracle, so describing a handful of decisions pays back immediately instead of after a full formalization. And a coding agent can do most of the typing, with a person reviewing what the definitions mean. Our friends' problem is still there, but the unit of work it applies to is now small enough to try on an afternoon. We'll show one with a [runnable Agda-and-Go example](https://github.com/yovico-ai/agda-guardrails), then say what happened when we applied the same arrangement to our own payment system. Some precedent first, because we're not the first to notice this. Beginning in 2011, AWS engineers used TLA+ and PlusCal to describe system designs and check them with TLC. Their published examples included S3, DynamoDB, EBS, and an internal lock manager. The listed models ranged from 102 to 939 lines, excluding comments. One DynamoDB defect had a shortest counterexample of 35 high-level steps and had escaped extensive reviews and testing. These were compact design models, checked by exhaustive state exploration. [The AWS account](https://6826.csail.mit.edu/2020/papers/formal-methods-amazon.pdf) also describes how they got engineers to try it at all: they avoided the words *formal*, *verification*, and *proof* and called the technique “Debugging Designs” and “exhaustively testable pseudo-code.” Engineers obtained useful results in two to three weeks, and models helped assess substantial optimizations. Later work moved closer to the implementation. The [ShardStore team at AWS](https://www.amazon.science/publications/using-lightweight-formal-methods-to-validate-a-key-value-storage-node-in-amazon-s3) (summarized in [an Amazon Science post](https://www.amazon.science/blog/aws-team-wins-best-paper-award-for-work-on-automated-reasoning)) used executable reference models written in Rust, generated input sequences, and additional checking techniques to validate an S3 storage component. Failures could be reduced to smaller reproductions. The work prevented 16 issues from reaching production. Reference models averaged about 1% of the corresponding implementations' code size, although the complete verification infrastructure was larger. In [*Escaping the Quicksand: A Call to Arms*](https://arxiv.org/abs/2608.19674), Peter Sewell and Jean Pichon-Pharabod argue for the same direction: executable specifications that can serve as test oracles, with progressively stronger checks as needed. They explicitly include adding specifications to existing systems, which matches our experience: making existing decisions precise can reveal that they were never as settled as the code made them appear. An ordinary application needs the same thing: a place to write the decisions down, and a way to ask the running code whether it follows them. Consider a subscription described as “active.” Does that mean the customer can use the product, or that billing should continue? A cancelled subscription may still grant access for an already purchased period. A failed payment may leave billing retries active while access is suspended. “Active” is answering two questions at once, and people who use the word rarely notice which one they mean. Our demonstration chooses four states and the following policies: | Membership state | Access allowed? | Billing active? | |---|---|---| | Active | Yes | Yes | | Cancelled, paid period remaining | Yes | No | | Payment retry window | No | Yes | | Expired | No | No | These are product decisions. Another product could reasonably allow access during payment retries, and nothing in Agda would object. The Agda billing definition is short enough to show in full, apart from its module declaration and imports: ``` BillingActive : MembershipState → Bool BillingActive active = true BillingActive cancelledPendingPeriodEnd = false BillingActive gracePeriod = true BillingActive expired = false ``` The first line says that the function maps a membership state to a Boolean. The remaining lines answer the question for each state. The access definition has the same shape, with different answers in the middle two rows. Nothing is being proved. There are four possibilities, each with an answer, and the checker can at least confirm that none of them was skipped. The repository's default branch, `broken`, contains a plausible mistake in the Go implementation. Billing follows the access rule: ``` switch s { case Active, CancelledPendingPeriodEnd: return true default: return false } ``` Its comment explains that members are billed while their membership remains live. The code agrees with the explanation. Its ordinary unit tests also pass: they cover the active and expired states, where both policies agree. We made the example up, but we have seen this shape of bug many times in real review. The comment matches the code, the tests pass, and the reviewer nods, because nobody is checking the decision underneath. To run it with Nix: ``` git clone https://github.com/yovico-ai/agda-guardrails cd agda-guardrails nix develop make check ``` The repository also documents a Docker route. `make check` checks and compiles the Agda specification, then runs the Go tests. The compiled specification is what connects the two. In the demo, the implementation is a small Go package. At Yovico it is the production application, written in Go and TypeScript, with its own databases, interfaces, and algorithms. In both cases the implementation is separate from the specification and need not resemble the model at all. We make the specification executable and use it as an oracle. In this demo, Agda's compiler produces a program that accepts a membership state and returns the two policy decisions. The Go harness keeps that program running and queries it over standard input and output. For each generated state, it asks the oracle for the expected answers, calls the Go implementation, and compares the results: ``` ┌─ compiled specification ─ expected result ─┐ generated input ───┤ ├─ compare └─ implementation ───────── actual result ───┘ ``` The expected values come straight from the specification we reviewed. Nobody translated it into Go assertions by hand, which is where the second copy of the same mistake usually appears. On the broken branch, the ordinary tests pass while the comparison can report: ``` BillingActive("cancelled_pending_period_end") = true, spec says false ``` The other possible counterexample is `grace_period`, where the disagreement runs in the opposite direction. Switching to the fixed branch changes the billing case list: ``` git checkout main make check ``` The same specification and test harness now agree with the implementation. Four states don't need random testing, and a plain loop would find this bug. The demo uses a property-testing harness because that's what you'd use once the domain grows, and we wanted the arrangement to be the real one. For a stateful system, such as our payment code, inputs become histories of commands: propose, accept, withdraw, retry, receive a delayed response. The model and implementation start from corresponding initial states and evolve separately under the same commands. The comparison may include success or refusal, the resulting payer, and whether another organization's state changed. Expected state must come from the model's own transitions. If you feed the implementation's own database state back in as the expected answer, the comparison is checking the database against itself. A model uses small identifiers and lists; the implementation uses UUIDs and SQL tables. The adapter between them has to translate faithfully, and that translation is part of what is being trusted. A 200 response does not show that the persisted payer is correct. For that, look at the database. An oracle can allow more than one result. Sewell and Pichon-Pharabod use a broader definition: given an observed behavior, it decides whether the specification permits it. Partial specifications and systems with several valid outcomes fit that definition. We check a constraint on an execution without specifying every detail of it. The evidence has limits, and it's worth being plain about where. The specification has to say what we actually intended; implementing a wrong rule consistently is still wrong, so the definitions and the scope of each theorem need a reader. The test campaign only covers what it generates: command sequences, concurrency schedules, and failures nobody thought to produce stay untested, and a provider simulator, ours standing in for Stripe, checks our handling of the responses we modeled, not the real provider's. And the adapter has to carry over what matters. The demo checks agreement on state names before it tests any decision; a larger system needs the same care for identities, state projections, and observed effects. A mismatch gives us an execution to investigate. It might be an implementation defect, an adapter error, or a problem in the specification. Keep the input and the exact revisions of model and implementation and it's reproducible; shrink the failing history and it becomes readable. Deliberate mutations, such as the demo's broken billing rule, check that the comparison can see the disagreements we care about. A finite campaign that passes tells you the two agree on the cases you tried. A proved invariant tells you about every state covered by the theorem. Those are different claims. Now try changing the requirements. The repository includes a patch that adds a fifth Agda state, `paused`, without changing the policies: ``` git apply demo/add-paused-state.agda.patch make check ``` Agda rejects the incomplete definition: ``` Incomplete pattern matching for AccessActive. Missing cases: AccessActive paused ``` What does pausing do to access? To billing? Agda has no idea, and it shouldn't. What it does is refuse to compile until someone decides. The corresponding Go patch builds fine: the existing default branch absorbs the new state and returns false, and nobody is asked anything. Go has exhaustive-switch linters that would complain too. The point is that something in the pipeline has to make the question visible, and then a person has to answer it. After the experiment, undo the patch with `git apply -R demo/add-paused-state.agda.patch`. We chose Agda because we wanted executable definitions and mathematical arguments in one general language, with room for further properties as the questions grew. Rocq and Lean offer similar breadth. [TLA+ organizes its language and tools around system behaviors over time](https://lamport.azurewebsites.net/tla/high-level-view.html), represented as sequences of states, a useful specialization. Agda lets us construct the abstractions we need, although it doesn't thereby supply TLC's automated state exploration. At [Yovico](https://www.yovico.ai/), payment already existed. While working with a coding agent to formalize payment responsibility, we found decisions in that existing system that needed more thought. Suppose Alice and Bob own the same organization. Alice pays its bills, and they agree that Bob should take over. To specify that operation, we have to say what changes and what remains unchanged. The organization's identity, credits, and billing history should survive the handover. Alice's other organization should remain unaffected. Those requirements made us re-examine existing representations. Our earlier design allowed organizations to share a Stripe Customer as a way of reusing a payment method. But a card and an organization's billing identity are different concepts. Sharing one did not require sharing the other. The revised design keeps a separate Customer for each organization that needs one for billing, even when the same person and physical card fund several of them. Usage accounting exposed another decision. The code resolved an organization's payer and drew on that person's personal credit pool. Asking what a handover must preserve forced a more basic question: whose credits were these? The ongoing work moves that accounting to the organization, so changing the payer does not redirect its balance. Checkout authority also needed to be reconciled with the explicit agreement about who pays. The payment system is still being reworked. Most of what we found so far came from arguing about the specification with Valentyn and the agent, not from anything the checker said. We count that as the tool working. We haven't proved anything about any of this yet. Writing it down exposed policy we hadn't settled, and that had to come first. Once it's settled there are real theorems to state: does every allowed transfer preserve the credits of every organization? Does every refused request leave the state unchanged? Does completing a transfer preserve every unrelated organization's payer? Such laws quantify over the model's admitted states and operations. Proving them is further work with the same tool. A coding agent can write a handler, the tests, and a convincing explanation, all from the same mistaken interpretation. Giving it another prose document helps only if that document actually resolves the ambiguity. An executable specification gives you something to read and, more usefully, something that can be wrong out loud when the code disagrees with it. An agent can have wide freedom over internal structure and algorithms as long as its observable behavior agrees with the settled rules; a disagreement is a concrete question, and if the rule is what needs changing, that's a product decision made in the open. An agent can help write the specification too, and Agda actively assists that work. In its [interactive mode](https://agda.readthedocs.io/en/latest/tools/emacs-mode.html), an unfinished proof contains holes. For each hole, Agda can show the exact goal and the assumptions available, split a variable into its constructor cases, simplify expressions, and refine a proposed proof into smaller goals. Automatic proof search can fill some holes. Many routine steps can therefore be obtained from the tool, while harder arguments still require guidance. The agent can ask Agda what remains to be established, request a case split, and check the next construction against the resulting goals. In our work, using that interaction makes the agent much more effective than repeatedly generating a complete proof and discovering at the end that it doesn't type-check. Coding agents tend to treat Agda as another implementation language and bring their testing habits with them. Asked to prove that a transfer preserves unrelated organizations, an agent may construct a particular world containing Alice, Bob, and two organizations, execute a transfer, and show that the second organization is unchanged. The file type-checks, and it has proved exactly one example. We have had to insist: regression cases belong in the implementation tests, and a preservation theorem has to quantify over every state and operation it claims to cover. Case analysis is fine as long as the cases cover the whole domain. Three convenient inputs with “therefore” in front of them are a test, not a proof, and Agda will happily accept them because it checks the statement that was written, assumptions and all. It can't tell that the agent quietly replaced our question with an easier one. You don't need to master Agda, or become a formal-methods specialist, before using this approach on a modest problem. Much of the day-to-day work resembles “vibe coding” an Agda specification: explain a rule, have the agent draft it, inspect what the checker says, and iterate. The part that deserves deliberate human attention is the meaning of the definitions and the scope of the claims. Learning enough to read those claims is a much smaller starting commitment than learning to construct every proof yourself. Running two programs independently doesn't make their assumptions independent. The demo includes a reusable skill that starts by asking the agent to extract a decision table from requirements and bring unresolved entries back for review. The table is small enough to discuss before the implementation gives each answer consequences throughout the code. The joke about two million words for a NAND gate assumes you have to use all of the machinery. You don't. Four states, two decisions, and a check that the code follows them is a complete, useful unit, and it took an afternoon. The fifth state turned up a question we hadn't asked; the payment system turned up several we thought we had already answered. We'd rather find those on a Tuesday than in production. P.S. We drafted this with a coding agent and edited it until it said what we mean. The ideas and decisions are ours, and so are any mistakes.