Toolchain: annotation-driven model generation for model-checking business logic (LLM + standard tooling + Specl)

[danwt]

Toolchain: annotation-driven model generation for model-checking smart-contract business logic

Summary

Specl's strength is checking business logic as a state machine. The barrier to using it on real systems (e.g. Solidity smart contracts) is the gap between source code and a faithful Specl model: writing the model by hand is slow, and a hand-written model silently drifts from the code it is supposed to represent.

This proposes a toolchain that closes that gap. It combines three kinds of component:

1. Standard program tooling (compiler AST, storage layout, static analysis, a test/execution framework) — deterministic ground truth.
2. An LLM — used only as a fallible translator/explainer, never as an oracle.
3. The Specl model checker — the trusted engine that exhaustively explores and proves.

The design principle is LLM proposes, the checker and the runtime dispose: the LLM drafts a model, and deterministic gates reject or repair it until it is provably faithful. The LLM is allowed to be wrong; the system catches it.

The problem with naive "LLM generates a model"

If you cannot trust the generated model, the model-check result is worthless. Full source → model extraction is also intractable in general (unbounded state, external calls, etc.). So the toolchain never trusts a generated model on faith — it makes fidelity machine-checkable and automatic.

Architecture

Three deterministic oracles bound the LLM, none of them an LLM:

1. Compile gate — the generated model must parse and type-check in Specl. Instant.
2. Conformance gate — replay traces (both randomly generated and enumerated from Specl's BFS frontier) against the real compiled contract in its native test framework, and assert the model's predicted next-state matches the contract's actual next-state at every step. This is refinement/differential checking, repurposed as the LLM's lie detector.
3. Regression gate — a corpus of known bugs must reproduce as counterexamples, and known-good code must verify.

If a model passes all three, the exhaustive + symbolic check on it is trustworthy. If the conformance gate fails, the concrete divergence (the trace, the model's predicted state, the contract's actual state) is fed back to the LLM to repair the model. Loop until conformance holds or a human is flagged.

Components

• Extractor (deterministic). Compiler AST + storage layout + static-analysis read/write sets per function. Produces a typed state skeleton and a per-action variable footprint. The footprint grounds the model's frame: if a generated action claims to write a variable that static analysis says the function never writes, reject before running anything.
• Drafter (LLM). Skeleton + existing property/fuzz harness + source + annotations → first-draft Specl model. Translation is what LLMs are good at.
• Compiler (deterministic). Annotations/model → Specl's generic transition-system IR → Specl.
• Validator (deterministic). Conformance replay in the target's native test framework.
• Checker (deterministic). Exhaustive BFS + symbolic k-induction/IC3.
• Narrator (LLM). Counterexample trace → human-readable bug report + severity + the offending source line + a generated reproduction test in the target framework.
• Repairer (LLM). Conformance divergence → model fix; loop.

The LLM appears only at Drafter, Narrator, Repairer. Every load-bearing verdict is deterministic.

Key ideas

The existing test/property harness is the Rosetta stone

You do not generate a model from raw source. Most serious contracts already ship a property/invariant fuzzing harness, which is a semi-formal model: its handler functions are the actions and its properties are the invariants, with bounds written down. Generate the first-draft model from harness + source, not from scratch — the abstraction work is half-done, and the LLM's job shrinks to filling in each action's transition body.

Annotation layer

Inline, doc-comment-style annotations on the source function describe its effect on an abstract state. Sketch:

/// @specl:action deposit(user, amount)
/// @specl:require amount > 0
/// @specl:effect shares := floor(amount * WAD / rate)
/// @specl:effect balance[user] += shares
/// @specl:effect totalSupply  += shares

A compiler lowers the annotations to the transition-system IR. Annotations are LLM-drafted, human-approved, machine-verified (conformance proves they match the code). They double as in-place documentation of each function's effect.

Anti-rot: conformance as a CI gate

Formal models usually die because they drift from code and nobody notices. Here the model lives next to the source, is reviewed like code, and the conformance gate runs in CI. Change the code so the model no longer conforms → CI fails → the model must be updated. The model cannot silently drift. Model-checking is cheap and deterministic enough to gate every change (unlike a long fuzz soak).

Larger directions

• Business-logic-first. Draft a Specl model from a natural-language spec of the rules before code exists, and let the checker find logical contradictions in the business rules at design time. Then reverse the pipeline: generate the implementation's harness and property tests from the proven model, with conformance binding them.
• Invariant library. Encode common bug classes once as Specl invariant templates; the LLM instantiates them per system.
• Invariant discovery. The symbolic engine's inductive strengthening yields machine-proven invariants that can be ported back into the target's own property suite — more grounded than LLM-guessed invariants.

Why Specl specifically

Randomized fuzzers sample the sequence space, cannot prove absence, and are nondeterministic (so they cannot be a hard gate). Bounded symbolic execution of bytecode proves per-input but is depth-limited and usually applied to stateless properties. Neither exhaustively explores nor proves a multi-step business-logic invariant. That is the gap this toolchain fills with Specl, and the conformance gate is what makes the abstract proof trustworthy against the real code.

---

Work breakdown

Split into what lives in this repo vs. what each adopting project provides.

Part 1 — Specl side (this repo)

Engine / IR:

• Aggregation builtins (sum / fold over a dict/set). Conservation invariants (totalSupply == sum(balances)) are unwritable without this today. Highest-leverage single feature for financial/business modeling.
• Fixed-point / rounding primitives: explicit floor/ceil integer division with a documented rounding direction, and a convention for scaled fixed-point values. Many real bugs are rounding/flooring bugs; without faithful rounding the model can miss them.
• Range/subtype widening so a 1..4 const fits where a wider range is expected (see existing type-unify gap), to reduce friction in generated models.

Generic toolchain infrastructure (language-agnostic, lives in core):

• A stable, documented schema for the generic transition-system IR JSON (the existing specl-ts), versioned, with a published JSON Schema so external adapters can target it.
• A conformance/trace-export interface: a command/format to emit (a) the full BFS frontier or (b) a single counterexample as a structured, machine-readable trace (action + params + pre/post abstract state) that adapters can replay against a target runtime.
• An annotation-spec format + reference lowering: define the @specl:action/require/effect mini-language and a lowering from it to the transition-system IR. Language-agnostic; adapters map their source comments onto it.
• A standard counterexample JSON output for the narrator/PoC-generator to consume.

Plugins / adapters (a plugins/ or adapters/ directory in this repo is fine):

• plugins/solidity/ — a Solidity adapter: extract state skeleton + per-function read/write sets from compiler/static-analysis output; parse @specl: annotations; emit transition-system IR; and a conformance runner that replays exported traces in a Solidity test framework and diffs abstract vs. concrete state. (Solana and other targets follow the same adapter contract later.)
• Reference invariant-template library (conservation, no-mint-from-nothing, monotonic accumulator, round-trip-no-inflation) as reusable Specl snippets.

Docs:

• A guide: "model-checking business logic from existing code" — the annotation format, the adapter contract, the conformance gate, and a worked end-to-end example.
• Adapter authoring guide (how to write a new target adapter against the IR + trace + conformance interfaces).

Part 2 — Target side (each adopting project provides)

• Author the @specl: annotations on the functions whose business logic should be checked (LLM-drafted, human-approved).
• Provide the model the adapter cannot infer: the chosen abstraction level (what to drop), bounds (number of actors, value ranges, fixed-point scale), and the initial state.
• A conformance harness in the project's own test framework that the adapter's runner drives: a way to apply an action with given params and read back the abstract state variables after each step.
• Wire the resulting model-check + conformance check into the project's CI as a gate.
• Maintain the model alongside the code (the conformance gate enforces this, but the fix is the project's).
• Optionally: a regression corpus of the project's own past bugs, expressed as invariants, to keep as permanent checks.