A methodology for building software where a formal model, not the code, is the source of truth. The code is derived from the model and proved to refine it; invariants are stated and machine-checked on the model; the parts of the chain that cannot be made formal are named explicitly rather than left implicit.
This document describes the methodology in general. A worked example (Tetris, specified in Rocq, implemented in JavaScript by this method) is at https://github.com/jskri/formal-tetris.
In conventional software development the code is the primary artifact. It is the thing that is true, the thing that runs, the thing that is maintained. Documentation, diagrams and specifications drift away from it over time, because they are secondary: when code and documentation disagree, the code wins, since the code is what executes.
This approach inverts that relation. The primary artifact is a mathematical model of the system. The code is derived from the model, the way a binary is derived from source. The model is the source, the code is the build output. Everything else in the method (invariants, an implementation document, a refinement proof, tests, a tower of refinements) exists to keep that inversion true against the constant pressure for the code to become the de facto specification.
This approach is in the tradition of classical engineering and has a skeleton in four steps:
- Specify the system.
- Prove its invariants.
- Derive an implementation from the specification.
- Check the conformance of the implementation to the specification.
The rest of this document explains what each step means, why each component is present, and what is gained. Examples are drawn from a Tetris implementation built this way, with formal models in Rocq and a JavaScript implementation derived from them. Tetris is used to illustrate, not because the method is specific to games.
A common reason formal methods are rejected is that they are presented as all-or-nothing: either you do the full machinery (formal models, machine-checked proofs, verified refinement) or you do nothing. That is a false choice: the method here is a dial, not a switch. You choose at which level to apply it, and you can move up later.
Some points on the dial:
-
Super light. You write and maintain only the requirements. The code is written by a human or generated by an LLM. You (or an LLM) periodically check that the code conforms to the requirements. Since the requirements are informal, there can be a delta between them and the code, and this check cannot be exact.
-
Light. You write the requirements and sketch a formal model using simple set theory, in the style of TLA+. The model does not have to be written in a formal language: it is a sketch. But you do state the invariants, because the invariants are the point.
-
Normal. As in light, but the (single) model is written in a formal language (TLA+, Rocq, etc.), with its invariants. The invariants are not proved. An LLM can give informal arguments for them (no machine-checked proof), which is quite affordable.
-
Full. As in normal, plus machine-checked proofs. LLMs increasingly help with formal proofs, so this is less heavy than it used to be.
In full, you can keep a single model or build a tower of refinements (see below). The tower saves time when the system is complex, because a single flat model would become unmanageable (think of how unmanageable a large program would be in a single source file).
The important property is that the cost is paid in proportion to the assurance wanted. A team can adopt the method at the level its resources and risk tolerance allow.
Specification does not begin with a formal model. It begins with a "definitions and requirements" document that gives the functional requirements in a hierarchical form. The requirements are structured as a tree, and each requirement has an id (a path in the tree) used for later reference, in particular from the formal model. In the Tetris models, definitions such as the score formula carry ids like req-score-formula, and the model construct that addresses a requirement is tagged with its id.
This linking is traceability, not validation. It is not possible to formally prove that a model meets its requirements, because the requirements are informal. The link between a requirement and the model construct that implements it rests on human reading. This is discussed further under "the two informal gaps" below.
The central artifact is the mathematical model. It describes the system to build and "implements" the requirements. This model is what is missing in almost all software projects.
The model gives an objective and non-ambiguous description of the system. Two things follow from having it, and neither is possible without it:
- The critical properties of the system can be expressed (the safety invariants, the liveness properties).
- Correct reasoning about the system becomes possible (the proofs).
"Objective and non-ambiguous" does not mean that every detail is fixed. That is not the role of a model. Think of a house blueprint that does not give the color of the paint on the walls. The blueprint is exact about what it specifies and silent about the rest, on purpose.
In the Tetris example, model T1 defines the core mechanics: a State (the grid, the current piece and its position and rotation, a gameover flag, a count of just-cleared lines), the transitions (MovePiece, RotatePiece, FixPiece, FallStep), and an invariant Correct that says the state is well-formed (correct dimensions, the piece sits on free blocks inside the bounds, no full line is left uncleared). The central theorem is that Correct is preserved: it holds at the initial state and is preserved by every transition.
Invariants are a choice. Safety invariants (nothing bad happens) and liveness properties (something good eventually happens) are both candidates. You decide which belong to the critical properties of your system, and whether to pay to check them. The Tetris models prove safety (invariant preservation). They do not in general prove liveness, with one local exception (a lemma stating that a fall step always succeeds when the game is not over). Liveness for the whole system would need fairness assumptions on the scheduler, which is a real addition. Whether to make it is a position on the dial, not an omission.
Once the model and its invariants exist, the implementation must be derived from the model.
Some proof assistants can extract executable code directly from a model (for example the Extract command in Rocq). This is not used here, and the reason is efficiency, not abstraction. You can extract from a very abstract model, but the extracted code is then usually unacceptably inefficient. To get realistically efficient code you have to refine the model heavily, replacing data structures and algorithms with low-level ones, and it is this refinement that is time consuming. Readability is a secondary concern, since generated code is normally not read, the same way the binary output of a compiler is not read.
Using an LLM cuts the refinement step. The LLM can optimize directly and aggressively, changing data structures and algorithms in one move rather than through a chain of proved refinements. The cost is the uncertainty the LLM introduces. This is the same trade discussed later under the compiler analogy: the LLM may optimize more radically than a verified extractor precisely because it justifies each output after the fact rather than relying on a fixed, proved translation scheme.
The implementation is generated from the model rather than extracted. The generator can be a human or an LLM; the Tetris example uses an LLM, and that is likely the common case, because writing the code and its proof by hand is a lot of work and an LLM is what makes the approach affordable. The rest of this document speaks of "the LLM" for concreteness, but the role is "whatever produces the code and its proof," human or machine.
Generation by an LLM brings a problem. LLMs are not deterministic, and they tend to "invent": they silently fill gaps in the specification, sometimes with results that surprise the designer.
Three things mitigate this:
- The formal model states the designer's intent without ambiguity.
- An implementation document (
implementation.md) records every implementation decision. - The generator is obliged to prove, in a
proofs.mddocument, that the generated code refines the model: that there is a refinement mapping (a homomorphism) from the code to the model.
So the generation is a function from two inputs to two outputs, carried out by one entity (human or LLM):
formal model × implementation.md → code × proofs.md
The third point is the load-bearing one. The refinement mapping is also a semantics: it gives the code an interpretation in terms of the model.
implementation.md records the decisions that the model deliberately leaves open, and the decisions forced by the target language. It is the document that makes the generation auditable rather than a black box: without it, the refinement proof would have to reconstruct every choice from the code; with it, the choices are stated where they can be checked.
When writing implementation.md, the typical questions to consider in the target language are:
- Are integers bounded?
- If so, can overflow happen? One solution is saturating arithmetic, at the cost of dropping strictly-increasing lemmas (e.g. that a line clear strictly raises the score). Another is to impose bounds on constants so that overflow cannot occur, when that is possible.
- Is the language's equality compatible with mathematical equality (value semantics), or must custom equality functions be written?
- The same kind of question for copying.
- If the generated code is imperative, does the order of assignments respect the data dependencies?
- And others, depending on the language: termination, behavior at the boundaries the model does not cover, concurrency, floating point.
Each of these has a different answer per language, which is exactly why they belong in implementation.md and not in the model. JavaScript is a sharp case, because it has no integer type at all: every number is an IEEE-754 double, exact only below 2^53. So the question is not "does an integer wrap" but "is this value still an exact integer." In the Tetris implementation the incremented fields (score, total cleared lines) could in principle leave the exact range, so they saturate at the maximum safe integer through a capAdd helper. Overflow is not expected during real play, but a proof obligation cannot appeal to "unreachable in practice": it has to hold for all inputs, so the case must be handled to keep the refinement total. implementation.md records the decision and its consequence (saturation preserves monotonicity but drops the strict-increase property once the cap is reached).
Note that implementation.md is not purely about how the code is written. A few of its choices (the saturating cap is one) can change the behavior specified by the model at the boundary. It is closer to "compilation flags plus a documented list of implementation-defined behaviors" than to flags alone.
proofs.md argues, construct by construct, that the code faithfully realizes the model under an explicit mapping. The mapping is a refinement mapping, i.e. a homomorphism: the model is a transition system (states, initial states, a labelled next-step relation), and the mapping must preserve that structure. Concretely it must satisfy two conditions:
- every initial state of the code maps to an initial state of the model;
- every step of the code maps to a step of the model.
In practice the second condition is handled by mapping the code's events to the model's events, which is sufficient as long as the state mapping commutes with the transitions (apply a code step then map, equals map then apply the mapped model step).
Under that mapping, proofs.md discharges the per-construct obligations: for instance with Tetris second model's implementation, the ordering of the in-place assignments in fixPiece (the model's simultaneous update becomes a sequential one, and the order must respect the data dependencies), the mapping of natural-number subtraction to a clamped Math.max(0, a-b), the correctness of the saturating-add helper, and so on.
Two properties of proofs.md matter.
It is active, not passive. Requiring the proof as part of the generation task constrains the generator during the work. It cannot make a refinement-violating choice without then failing to justify it, so the obligation steers it toward choices that are justifiable. The proof is not only evidence collected after the fact; it is a generation-time constraint that improves the output. The requirement to prove something changes what gets written, the way a mathematician asked to prove a theorem states it more carefully than one asked only to assert it. So the obligation makes the generator more trustworthy, rather than merely auditing an untrustworthy one after the fact.
It is checked by a human. When the generator is an LLM, proofs.md is produced by something unreliable (LLMs hallucinate), so the proof itself may be wrong, and a human must check it. (The machine-checked proofs of the method concern the model, not the code; the refinement proof is the part that is not machine-checked here.) Human proof review is not exhaustive (it can miss a wrong step the way code review can miss a bug) which is why the differential oracle exists as a second, independent check on the same boundary. This has a direct consequence for the form of the document: a human-checked proof must be readable and modular, and must make its load-bearing steps explicit instead of burying them. Naming each obligation, separating the routine from the subtle, and flagging exactly where a non-obvious step occurs are important. A correct but unreadable proof partly defeats the purpose, because the human checker cannot efficiently locate the steps that could be wrong.
A note on what "wrong" can mean here. By definition, correct code is code that refines the model, so there is no such thing as wrong code that nonetheless refines the model. Two distinct failures are possible. Either the proof is wrong (the code does not actually refine the model, and the human check or the tests should catch it), or the code refines the model but the observed behavior is still not what was wanted, which means the model itself is wrong or under-specified. The second case is not a proof failure; it is the requirements-to-model gap discussed below.
The previous points have a direct operational consequence. If generated code may be edited by hand, then the code, not the model, becomes the truth again, and every guarantee that depends on "the model is the source" is void. The refinement proof certifies the code as generated; a later manual patch is uncertified, and the certification cannot be transferred to it.
So the rule is: generated code is never hand-edited. To change the code, change the model or implementation.md and regenerate. This is the operational heart of "the model is the source." It is also the rule a tired practitioner breaks first, because patching the output "just this once" is faster than regenerating. Breaking it silently dissolves the approach, which is why it has to be stated as a hard constraint, on the same level as the proofs. A developer would never hand-edit the text section of a binary produced by a compiler; the same discipline applies here, for the same reason.
In the full setting it is generally better to generate code early, before all invariants and refinements are proved. The reason is the adequacy problem: is the model really capturing the right things? A model can also contain logical errors (for example, forgetting to merge the fixing piece into the main grid, so that a piece simply disappears once it is fixed). Early generation is a quick check on both adequacy and logical errors, and it can save a lot of time.
Proving properties at an early stage surfaces bugs and also surfaces under-specification (missing or too-lax axioms), which is a failure mode testing essentially cannot catch: a test exercises behavior that exists, but it cannot reveal that the axioms permit a model that was not intended. In the Tetris work a logic error in one model (a line-count defined as a difference that was identically zero under the invariants) was found exactly this way.
The code is proved to refine the model, so there is good reason to believe it is correct. But this belief depends on proofs.md, which (when the generator is an LLM) is not machine-checked, and it depends on a correct understanding of the target language, where it is easy to overlook something (reference semantics for complex data types but value semantics for basic ones, for instance). So tests are needed.
The conformance check uses unit tests, property-based tests, fuzz tests, and an oracle. The most informative of these is the oracle, which makes the check differential: a second, independent implementation of the model is written to be as simple and obviously correct as possible (no mutation, no performance concern, a direct transcription of the model). The engine and the oracle are run on the same random event traces, and their full states are compared at every step. A divergence is a conformance failure. There are no hand-written expected values: the oracle produces the expected answer dynamically, which is what makes the check scale to complex states over long traces.
Differential testing against a model-derived oracle is an instance of model-based testing, a known technique. Its specific role in this method is precise: it backstops the one non-machine-checked link in the chain (proofs.md). It cannot make the refinement proof machine-checked, but it provides independent empirical evidence against errors in that proof, since the oracle is written from the model, not from the code. This is why the tests are not a bonus. They are the rational hedge for the informal boundary that the choice of generation (over extraction) introduces.
It is worth being clear about what tests can and cannot do, relative to proofs:
- Tests exercise a sample of cases. Proofs cover all cases.
- Tests typically check local properties. Models and proofs address global invariants.
In complex systems (distributed systems are the clearest case) the gap between a global invariant and a local test is not a matter of degree but of kind, and testing alone does not prevent critical bugs.
Features can be introduced into the model progressively. In this case, there is not one model but several, each adding a set of features and formally refining the one below it. These models then form a tower.
In the Tetris example, T1 is the core mechanics and T2 refines it by adding score, level, and combo. T2 embeds T1's state as a field and adds the new scalars; a refinement mapping shows that every T2 transition projects to a T1 transition, so the correctness established for T1 propagates up. Further models address the remaining requirements: hard drop, ghost piece, hold/swap, next-piece preview, the seven-bag randomizer, and wall kicks.
The tower exists for the same reason source code is split across files. A single model containing core mechanics, scoring, hold, preview, randomization, and wall kicks all at once would be unmanageable, and so would its proof. The refinement boundaries keep each model and each proof tractable. For a complex system the tower saves time rather than costing it.
Two of the remaining models are worth noting as stress tests of the method. Wall kicks are table-driven and easy to get subtly wrong, which is exactly where a formal model earns its keep and where under-specification (an axiom that is too weak) tends to hide. The seven-bag randomizer introduces the first genuinely stochastic element, which is a modeling decision and not just another feature: it forces a choice about how the specification represents environmental nondeterminism (as nondeterministic choice, or as a parameter threaded through the transitions the way the next piece already is).
The shape is a compiler: the model is the source, implementation.md is the compilation flags (plus a documented list of implementation-defined behaviors), the code is the binary. The one piece with no ordinary-compiler counterpart is proofs.md, and seeing why sharpens two things.
The reason an ordinary compiler has no proofs.md is trust. You trust that the binary refines the source because you trust the compiler, validated once and globally by long use. A verified compiler such as CompCert makes this a theorem, proved once and for all. Here the "compiler" is an LLM, which cannot be trusted once and for all, so the semantic-preservation obligation must be discharged for every output. proofs.md is the certificate that this particular translation was faithful. The closest named concept is proof-carrying code: the producer ships the artifact together with a proof that it meets the required property, and the consumer checks the proof instead of trusting the producer. The only weakness, already discussed, is that the checker here is human rather than a machine. This also reframes the no-hand-edit rule in one line: you do not edit the binary a compiler produced, and for the same reason you do not edit generated code, because the certificate is attached to the output as generated.
The analogy also explains the optimization freedom claimed earlier (under "why not code extraction"). A verified compiler restricts the optimizations it performs to the ones its once-and-for-all theorem already licenses; it will not replace a list with a hash table or swap in a better algorithm, because its proof is tied to specific local translation steps. The LLM is bound by a weaker, more global constraint: only the observable behavior (the refinement to the model) must be preserved, and anything internal is fair game as long as the refinement holds. So the LLM occupies a strictly larger optimization space, and it can afford to precisely because it proves correctness anew for each output rather than relying on an advance theorem. The two are dual: a verified compiler constrains the optimizations to amortize one proof; the LLM constrains nothing and amortizes nothing, proving per instance instead.
The wider optimization space puts more weight on the model's notion of "observable" being the right one. A radical internal rewrite preserves observable behavior only with respect to what the model treats as observable. If something the model leaves unobservable is in fact observable to a real user (timing, memory, an iteration order that leaks), the rewrite can cross a boundary the proof does not police. This connects back to the question of whether the model captures the right things.
Because the language-specific decisions live entirely in implementation.md and proofs.md, the same model can target different languages. Keep the model, write a different implementation.md, and generate code in OCaml, C++, Rust, or another language instead of JavaScript. This is the structure of a retargetable compiler: one frontend (the model), many backends (one implementation.md per language), each emitting code plus a refinement proof for that language.
This separates cleanly what is language-invariant from what is language-specific:
- The model, the invariants, and their machine-checked proofs are written once and are target-independent. They are about the system, not about any implementation of it.
- Everything that varies between targets is confined to
implementation.mdandproofs.md.
The implementation-concern checklist from earlier (bounded integers, overflow, value versus reference equality, copy semantics, assignment order) is exactly the set of questions whose answers differ per language, which is why it lives in the per-target document. Rust's ownership nearly removes the aliasing and copy questions; C++ makes them sharp; JavaScript has no integer type at all (every number is a double, exact only below 2^53) while OCaml's native ints or a bignum library change that answer again. The refinement proofs differ per target too, but they discharge the same obligations against different language semantics, so the conceptual content is shared and only its discharge is per-language. A Rust backend's proof can be shorter on the aliasing obligations (the borrow checker discharges them) and must instead address its own.
The real limiting factor is the LLM's proficiency in the target language, and specifically its command of the language's semantics, not just its syntax. Ubiquitous languages like JavaScript or Python are well represented, so the subtle points the proof must address are within reach. An obscure language (say ATS) is problematic, and the failure mode is the dangerous one: not "cannot produce syntax" but "cannot produce a correct refinement argument," which corrupts the certificate.
Different targets can resolve the model's unspecified points differently, and legitimately. The saturating cap is a JavaScript-specific resolution of an overflow behavior the model left open; a Rust target might resolve the same point with checked arithmetic that panics, or a wider integer type, or a bignum. So two backends can be observably different while both refining the model, agreeing on everything the model observes and diverging only where it is silent.
This is not a problem to be mitigated. It is the method working as designed: you cannot complain about what you did not specify. If cross-target divergence at some point matters, the fix is to tighten the model so that it observes the thing you want consistent, which pushes the decision back to the single shared frontend rather than coordinating the backends. Resolving it at the backend level would quietly relocate authority away from the model and into a negotiation between implementation.md files, which is the inversion-breaking move the whole method exists to prevent. The only sanctioned place to resolve an unspecified behavior is the model.
The chain of trust is:
requirements → model → (machine-checked proofs) → implementation.md → code → proofs.md → tests
Most of this can be made formal. Two boundaries are informal, but for different reasons. The method concentrates the informality at these two points rather than letting it diffuse through the whole development.
-
requirements → model. This gap cannot be made formal, in principle. Informal intent cannot be formally validated against anything; it can only be traced (each requirement id linked to the model construct that addresses it) and reviewed by a human. The same gap exists in the B method, which traces requirements rather than validating them. No methodology can close it, because it spans the divide between informal intent and formal specification.
-
model → code. This gap can be made formal: code extraction closes it, and the refinement becomes correct by construction. It is left informal here by choice, to avoid the cost of extraction (detailed models, unoptimized code). The approach trades a machine-checked refinement for a generated, human-checked one (
proofs.md) to keep models concise and code efficient. The tests exist to backstop this specific boundary.
So only the first gap is irreducible. The requirement-to-model link rests on human judgment by necessity; the model-to-code link rests on a checked proof by choice, hedged by tests; everything between and around them is formal.
When the four steps are followed strictly, the method removes a structural cause of low quality present in most software projects. Without a formal model you cannot state global invariants credibly, so most projects do not have them. The consequence is not only lower confidence, but a structural blindness: a practitioner cannot see when an invariant is violated, because the invariant was never articulated. Bugs then surface only at the technical level (a crash, a wrong value), disconnected from the conceptual level (which invariant was broken). Two concrete failures follow:
- Problems are detected much later in the development cycle, because there is no invariant-violation signal at the moment of breakage.
- Fixes are inappropriate, because they patch the technical symptom rather than the conceptual cause.
A model makes global invariants expressible; expressibility makes violations detectable; detectability moves bug discovery early and to the right conceptual level. That correctness is also explained (you know why the software works, because the invariants are proved) is a corollary of this mechanism, not an independent claim.
Is this overkill for Tetris? For a game, in isolation, perhaps. But the work is a methodological proof-of-concept, and the value of a proof-of-concept is to apply the method to a real, tangible, non-mathematical example that a reader can grasp immediately.
Two things should temper the "overkill" reaction. First, Tetris is deceptively simple. The rules fit on a page, but getting them exactly right (combo counting, wall kick rotations, garbage in multiplayer mode) is not trivial, and the method found a real bug in the specification during this project. Second, the full requirements addressed by the complete tower (hard drop, ghost piece, hold, preview, randomizer, wall kicks) are where the method's scaling argument and its handling of fiddly, error-prone features are exercised.
There is also a limit to what a proof-of-concept on a game can show. The method's cost is front-loaded (requirements, model, invariants, refinement proofs, much of it before there is running code), though the "generate early" practice mitigates this by producing running code well before the proofs are complete. The clearest return is immediate rather than delayed: the system works on arrival, and you know why it works, because the invariants are proved. This is the opposite of the usual paradigm, where you quickly get something that mostly works and then spend a long time making it converge toward something that works, often without ever quite arriving. Here you reach a working system and have the reason it works in hand. There is a further return over the maintenance lifetime (invariants catch regressions, the model makes the blast radius of a change visible, a refinement boundary localizes a feature), but the immediate return (correctness on arrival, and the predictability that comes with it) is what a proof-of-concept on a small system can already show.
-
J.-R. Abrial, on correct-by-construction and faultless systems (the B method and Event-B). See https://wp.software.imdea.org/cbc/wp-content/uploads/sites/5/2020/01/faultless-systems.pdf
-
Conal Elliott, denotational design: choosing a mathematical meaning for each construct and deriving the implementation to respect it. The refinement mapping used here is such a meaning.