Groovy 6 features for formal method advocates

How much confidence can you have that your code is correct — not "passes the tests we thought to write", but correct for every input?

On the JVM the usual answers are types, tests, and code review. Each helps; none of them proves a postcondition holds for all inputs, that an index can never go out of bounds, that a class invariant survives every mutator, or that a lock-free buffer stays in bounds under every thread interleaving. The discipline that does make those claims — formal methods — has long felt like a separate world: a different language (Dafny), a comment dialect bolted onto Java (JML), or a proof assistant you drive by hand (Isabelle, Lean).

This post is about how much of that world is reachable from ordinary Groovy 6 — and it is more than you might expect. As a taste: that is runtime metaclass programming below, verified against an exact specification at compile time — and when the spec is wrong, the compiler answers with the input that breaks it:

(How a metaclass method can be type-checked at all, let alone proved, is a story for later in the post.)

Two things matter, and it is worth being precise about which is which:

The relationship between the two is the thread running through this post. groovy-verify is not a fork, not a new language, and not a re-spelling of your specs. It reads the same @Requires/@Ensures/@Invariant you’d write for runtime checking, and it activates the same way every Groovy 6 type checker does:

So there is a genuine on-ramp here, not a cliff. Start today with groovy-contracts and the in-tree checkers — runtime-checked contracts and flow-sensitive null analysis cost you nothing and read like documentation that can’t drift. When you want a particular method or class to carry a stronger guarantee, add the verification extension over the contracts you already wrote — or, increasingly, ask your AI coding agent to do it for you. groovy-verify was deliberately built to be discoverable by agents: its diagnostics are machine-readable, its capability surface is documented for tools to consume, and a refuted proof can print itself back as a runnable failing test. We come back to that in Designed for humans and agents.

A note on versions before we start: groovy-verify tracks Groovy 6 closely, and the recommended pairing is Groovy 6.0.0-alpha-2 or later. Everything below was written against that pairing.

The audience for this post is Groovy and JVM developers who want more confidence in their code — not people who already speak the language of verification. So a short glossary, which the rest of the post leans on:

One Groovy nicety worth flagging: specs often want logical implication, and Groovy 5+ has the ==> operator for exactly that (a ==> b is !a || b), with a.implies(b) as the method twin. It reads naturally inside a contract closure — result >= 0 ==> a[result] == value — and you’ll see it throughout below.

Before any prover enters the picture, Groovy 6 already moves the needle.

The groovy-contracts module — long available, and enhanced in Groovy 6 to work in scripts and on loop statements — lets you attach executable contracts to methods and classes:

These are checked at runtime: violate a precondition and you get a precise assertion error at the boundary, not a mysterious failure three frames deeper. Crucially, they are also documentation that cannot drift, because the compiler weaves them into the bytecode — the contract and the code can never disagree without the assertion firing.

The newest member of the family closes the quadrant Design-by-Contract has historically left to javadoc prose: exceptional behaviour. @ThrowsIf (GROOVY-12135, landing in the next Groovy 6 pre-release, with woven/direct members on @Requires following as GROOVY-12136) states that a method throws a given exception exactly when a condition holds — and, by default, generates the guard for you, the general form of the pattern @NullCheck already provides for the null-check special case:

One line replaces the guard-clause boilerplate every service method opens with; woven = false documents a hand-written guard instead, and an optional checked mode verifies the iff at runtime in the same assertion style as @Ensures. The distinction it makes first-class is one the ecosystem has lacked: a @Requires violation is the caller’s bug; a @ThrowsIf throw is defined behaviour callers may rely on and catch. And its pedigree is this post’s story in miniature — the annotation was prototyped and battle-tested in groovy-verify (where the prover checks both directions of the iff), then contributed upstream, so the verification research fed the language itself.

Alongside the contracts, Groovy 6 ships a family of type-checking extensions — opt-in static analyses activated per class or method, each owning one narrow property:

They share one activation mechanism and compose freely: @TypeChecked(extensions = ['groovy.typecheckers.NullChecker', …​]). The companion post Groovy 6 features for Functional Programmers covers these in depth.

The reason this matters for a formal-methods audience: the contracts and the SPI are the foundation everything below builds on. groovy-verify adds no new annotations of its own for the core work — it reads these — and it registers as just another extension on the same SPI. So the step from "runtime-checked contracts" to "machine-proven contracts" is genuinely additive.

Here is the move. Take a contract you might already have written, and turn on the verification extension. Now Z3 checks the body satisfies the postcondition for every input — and when it doesn’t, the build fails with the exact arguments that break it:

That one verifies. Flip the body to return the wrong branch and the compile fails:

No test wrote max(-1, 0); the solver found it. This is the whole pitch in miniature — a proof is the spec, the spec is an ordinary groovy.contracts annotation, and a failed proof is a concrete failing input, not a shrug.

The informal one-liner the project uses is "Dafny for Groovy", but the closer structural analogue is Verus: rather than being a new language with its own compiler (Dafny), it verifies an existing mainstream language by embedding in that language’s native extension mechanism — Rust’s attribute macros for Verus, Groovy’s @TypeChecked extension SPI here.

Postconditions are the headline, but a lot of everyday value is in the implicit obligations — the ones you never wrote down because they’re "obvious". An index must be in bounds; a divisor must be non-zero; a reference must be non-null. groovy-verify discharges these from the contracts in scope, and refutes them with a counterexample when it can’t.

An unguarded array access:

The canonical example is Joshua Bloch’s binary-search bug — the midpoint (low + high) / 2 overflows once the array is large enough and returns a negative index. It lurked in java.util.Arrays for nine years. With overflow checking opted in (@CheckOverflow, off by default since Groovy integers are mathematical by default), it is a compile error:

The one-character family of fixes — compute the midpoint without overflowing — verifies clean:

The same overflow trap bites the textbook one-liner everyone "knows" is fine — absolute value is non-negative, except at Integer.MIN_VALUE:

Null safety falls out of the same machinery. Groovy idioms participate — here the safe-navigation operator narrows nullity, so no null obligation is left open:

Toy int functions are where verification demos start; real adoption needs it to speak the language of your domain. A representative sweep.

Money that is conserved. The property that matters in a transfer isn’t "the arithmetic ran" — it’s that no value was created or destroyed:

Change the body to bob = bob + amt - 0.01 — the "salami slice" fraud — and the @Ensures refutes. And because the numbers are BigDecimal, the proof is over exact decimal arithmetic. groovy-verify models each numeric type faithfully, which lets it prove the famous discrepancy outright:

Stateful objects that obey their own rules. A class invariant is established by every constructor and preserved by every mutator, so the whole object verifies as a unit:

Drop the constructor’s @Requires({ m > 0 }) and even construction is refuted — the solver finds the instance that violates the invariant before any method runs:

Aliasing — the bug value-semantics tools miss. Two parameters can be the same object, and a postcondition that forgets it is wrong:

The fix is to require distinctness — @Requires({ a !== b }) — and the proof goes through. groovy-verify models flat object fields with identity keys, so a write through one reference is seen through another exactly when they are the same object.

Loops are where verification earns its keep, because they’re where tests are least exhaustive. The contract is a loop @Invariant plus a @Decreases measure. The simplest shape:

The invariant pins i to its range across every iteration; the measure n - i strictly drops, proving the loop terminates; together they discharge the postcondition that the loop runs exactly n times.

That scales — all the way to a real, in-place sorting algorithm proven sorted and a permutation of its input (no elements invented or lost), under a sound @Modifies frame. The every, count, and old are all plain GDK Groovy; the @Decreases turns each recursive call into a proof by induction:

That a.count(v) == old.a.count(v) is the multiset-conservation property no test could exhaustively check. The same depth reaches Dijkstra’s Dutch National Flag (a three-way partition proven sorted-and-permutation from a four-region loop invariant) and a depth-first search proven for termination, soundness, coverage, and completeness — the benchmark proofs the Dafny community uses as credentials, here as worked examples in the repo’s five-act tour.

groovy-verify owns a narrow, deep slice — SMT-backed functional verification — and it deliberately composes with the in-tree checkers rather than duplicating them. The clean division of labour: the siblings own shape and syntax; groovy-verify owns the laws and semantics. All on one class, under one @TypeChecked:

Four extensions, four distinct jobs: MonadicChecker shape-checks the DO comprehension, PurityChecker checks the side-effect freedom of the @Pure some/none, NullChecker checks nullness, and groovy-verify proves the five monad/functor laws from the @Monadic annotation alone. All four compile quietly because this Maybe really is lawful.

That last gap is where even strong type systems stop. Haskell’s Monad and Scala’s cats.Monad enforce the shape of flatMap/pure but not the laws — a lawless instance type-checks in both, the laws left as a documented obligation. Proving them at compile time is something a type system structurally can’t do. The same split shows up with the combiner checker, where groovy-verify proves the monoid laws Z3-side from a @Reducer annotation:

A bad annotation fails loudly: @Reducer on subtraction refutes with Cannot prove @Reducer associativity for combiner sub — because (a-b)-c ≠ a-(b-c). The regex checker pairs the same way: RegexChecker validates that a pattern is well-formed syntax, groovy-verify proves what the match means, both reporting only their own kind of error in one compile.

Concurrency is the domain where "it passed the tests" inspires the least confidence, because the bug you fear appears once in billions of runs. This is where verification has the most to offer — and where it is most important to be honest about what a single technique can and can’t see.

`groovy-verify’s position is that a compile-time proof is one rung of a concurrency argument, not the whole of it. The proof is local and sequential; trusting it against a real running system means climbing two more rungs. Each trades coverage for fidelity, and none subsumes the others:

How the local proof works is rely/guarantee reasoning: each thread’s steps must uphold its @Guarantee (what this thread promises to do to shared state) while tolerating peer interference described by @Rely (what other threads may do). If every thread’s guarantee is also a peer’s rely, the conjunction holds globally under any interleaving — so you get two-threaded reasoning from a sequential proof, without modelling the scheduler.

A monitor-style account shows the proof’s transparency to Groovy’s lock AST transforms — the verifier sees the clean body before @WithWriteLock weaves in locking, and proves the invariant is preserved across the critical section:

Now the sharp edge — and the reason rungs 2 and 3 exist. Consider a counter meant to never exceed 1:

Rung 1 proves the invariant: sequentially, the guard keeps count in {0, 1}. But it is not thread-safe — two threads can both read 0, both pass the guard, and leave count == 2. The verifier proves the identical invariant for this broken version and for a @WithWriteLock version; the lock is transparent to a sequential proof, so it cannot tell them apart. Rung 3 (jcstress) separates them empirically: the unlocked counter reaches 2 about 5 times in 7 billion runs; the locked one never does. That 5-in-7- billion gap is precisely the kind of bug testing almost never surfaces — and exactly the gap the upper rungs close.

The bug becomes visible the moment you move to the real bytecode. A single-producer/single-consumer buffer that publishes before writing —

— proves the same bounds invariant as the correct "write first, publish second" version (rung 1 can’t see the race), but Lincheck (rung 3) catches it as a linearizability violation with a minimal trace:

poll() returns 0 — a value never offered. The lesson is the framing: verification raises the floor (the local invariant really is proven), and the model checker and bytecode tools cover what a sequential proof structurally cannot. The repo’s three-rungs write-up and concurrency examples carry the full set, including seqlocks and a lock-free bounded counter.

Where rung 1 reaches further. The framing above — rung 1 proves the local half, the upper rungs the rest — has an instructive exception. Leino’s Modeling Concurrency in Dafny casts a ticket lock for mutual exclusion as atomic events over a system invariant; ported to groovy-verify (walked through in full in the repo), rung 1 SMT-proves the structural properties directly. Mutual exclusion (at most one process in the critical section) verifies in both of the paper’s formulations — for the fixed two-process instance and for a symbolic process count, with Leino’s own quantified invariant (ticket uniqueness lands as a nested bounded quantifier). The fair-schedule liveness — a hungry process eventually enters: the "eventually", not merely per-call termination — runs Leino’s proof-loop at the same generality: the lock’s transition relation is spelled over a time-by-process state, and a recursive lemma walks a waiter at any ticket distance down to zero, each round’s progress derived from the relation (the served process’s scheduled Leave advances the display), not assumed. What stays hypothesized, by design, is the ∃-half of fairness — the witness times at which the scheduler runs each process, and the round-holders' identities — the same trade Leino’s GetTicketHolder lemma makes when it returns the holder rather than asserting one exists. Here rung 2 changes role: a Ticket.tla model has TLC enumerate every interleaving at three processes — which discharges exactly those witnessed facts (TLC derives scheduling and framing from the transition system, taking nothing as hypothesis) and confirms the same invariant on every reachable state. Two independent methods on one artifact, with a clean division of labour: the proof covers any process count symbolically; the model checker validates the witnesses exhaustively for a concrete one.

The breadth here is well past what one post should reproduce in full, so a tour of the rest — each with a one-line pitch and a worked example in the repo for when you want it.

And with the industry’s focus on security sharpening — AI-accelerated threats, supply-chain risk, and a shift toward secure-by-design — it’s useful to have another tool in that space that shifts whole bug classes left, several of them (overflow, out-of-bounds access, the salami-slice fraud above) squarely security-relevant and one aimed at security head-on:

Information-flow security (noninterference). You can label data High or Low and prove that a secret never reaches a public sink — directly or via control flow. Noninterference means a secret never influences anything an observer can see; the verifier tracks labels through assignments and branches and refuses the leak:

A Declassify.to(…​) construct marks the deliberate, greppable points where a controlled release is allowed.

Dimensional analysis (the Mars Climate Orbiter bug). Physical units checked at compile time — you can’t add kilograms to metres, and length / time must be a speed, not an area. One layer deeper, it catches the scale bug that sank the Mars orbiter: two quantities of the same dimension at different scales. Built on JSR 385, it recovers the SI magnitude and proves the exact read:

Liskov behavioural subtyping. An override may only weaken a precondition and strengthen a postcondition — never the reverse. A GoldAccount that accepts a larger overdraft verifies as substitutable; a RestrictedAccount that demands a minimum balance is refuted, with the input that breaks substitutability.

Even (some) dynamic Groovy. Everything above lives in Groovy’s statically checkable subset — @TypeChecked is the front door, so runtime metaprogramming has been out of scope by construction. But Groovy’s type checking is extensible in two directions: an extension can strengthen checking (groovy-verify itself is exactly that), and it can selectively relax it — type what looks like uncheckable dynamic code when there is evidence to type it from. The experimental metaprogramming pack does both at once: when an ExpandoMetaClass registration is spelled out in the same class, it types the registration and its use sites under @TypeChecked, then inlines the registered closure into the proof. The metaclass FizzBuzz examples from FizzBuzz with Groovy and emojis verify against exact specifications this way:

(That’s a script: the registration is a plain top-level statement — only the method is @TypeChecked, and the pack finds the registration in the script body.)

The gate is deliberately narrow and evidence-backed: no visible registration, no blessing — the code stays a compile error, exactly as @TypeChecked demands.

Functional proofs, Verus-style. Not everything needs a loop invariant: a method’s own @Ensures is assumed at its recursive call sites (sound because @Decreases proves termination) — which is proof by induction — and a void method whose only job is to carry an @Ensures acts as a lemma or theorem. The repo’s functional leftpad proves all three of the classic challenge properties this way, with a structural specification (result == pads(pad, n - s.length()) + s — the output is the padding block followed by the original string) and the length property derived from a padding-length lemma by a theorem method — the spec-function / proof-function structure of Verus, done with plain Groovy methods.

And, more briefly, the repo also demonstrates:

The full, honest inventory — every capability with its phase tag and its "deferred" edge — is in the repo’s CAPABILITIES.md, and the modelled-fragment boundary in FRAGMENT.md.

The throughline of Groovy 6’s "designed for human and AI reasoning" story is that a machine-readable, compiler-enforced contract is a specification a reader can trust without opening the body — and that "reader" is a human and an agent on the same footing. For the human, a method’s contract is documentation that can’t drift and a stronger claim than a comment: a postcondition groovy-verify has discharged is proven, so a teammate reviewing the signature, or you returning to it months later, can reason from it without re-deriving the body. For an agent, that same proof is a fact it can build on rather than a hint it has to second-guess. The functional-programming post showed agents mechanically deriving property-based tests from annotations; verification sharpens the same idea for both audiences.

groovy-verify leans into this deliberately. It was built so its capabilities are discoverable — the diagnostics are structured, the capability surface is documented so a person browsing the repo or a tool parsing it find the same answers, and a set of environment-variable knobs turn the checker into something you can hold a conversation with, whether you’re at the keyboard or an agent is. None of them change what is proven; they change what is reported:

For an agent, @ThrowsIf deserves a special mention in this story: "when does this method throw?" is exactly the question an agent otherwise answers by parsing javadoc prose or traversing bodies — unreliable, and expensive in context. A @ThrowsIf arm is one structured, enforced line (condition, type, direction), and the shipped JDK specs mean the agent often doesn’t need to consume it at all: write int i = s.indexOf(c); return s.charAt(i) and the compiler refutes with the -1 sentinel — JDK trivia an agent might hallucinate becomes an obligation the build enforces.

This is the practical shape of the on-ramp from the introduction. A developer adopts groovy-contracts and the in-tree checkers today. When a method deserves a stronger guarantee, adding the verification extension is a local, additive change over contracts that already exist. "Add @Ensures here and prove it; if it’s refuted, paste the suggested @Requires and add the repro test to the suite" is a tight loop you can run yourself at the keyboard — and, increasingly, one you can hand to an agent, with `groovy-verify’s machine-readable output as the feedback the agent closes the loop against.

To keep the honesty front and centre:

The honest summary the project itself uses: experimental Verus for the JVM, with Dafny-style specifications — distinctive in that its specs are ordinary executable groovy.contracts, so unproven obligations degrade to runtime checks rather than vanishing, and that its verifier composes with the other type-checking extensions.

For a formal-methods audience, the comparison set is the auto-active verifiers, with the Groovy column being groovy-contracts + groovy-verify together.

The point of the table isn’t that groovy-verify outranks Dafny or SPARK on maturity — it plainly doesn’t, and it is honest about being a fragment. It is that the JVM has lacked a modern, ergonomic, auto-active option — native annotation syntax, executable specs, counterexamples-as-compile-errors, delivered through the standard extension SPI rather than a separate build tool — and that gap is now, experimentally, filled.

The formal-methods world is closer to everyday Groovy than its reputation suggests, and the path in is gradual rather than all-or-nothing:

You don’t have to think about weakest preconditions or proof obligations to start. Write down what your method promises, let the compiler check it, and let the solver find the input you didn’t.