How Blockchain Works | Formal Verification and Model Limits

Imagine a fictional library with three digital borrowing passes. Its designers want to prove that the software never allocates more than three passes at once.

That is a specific proposed property. It is different from saying “the library system is safe”, which leaves the meaning of safe unresolved.

Formal verification begins by turning requirements into precise statements and reasoning about whether the relevant system satisfies them.

The first difficult task is therefore not pressing a prover’s button. It is deciding what should be true, at which points, for which behaviours and under which assumptions.

A beautiful proof of the wrong sentence does not establish the promise users actually needed. Precision about the question is part of the work, not a decorative introduction to it.

Contents · Next chapter

A test runs selected inputs or execution sequences and checks the observed result. Finding a failing example is valuable evidence that a proposed property does not hold in that case.

A formal method can instead reason about a defined collection of possible behaviours, depending on the technique and its scope. It may establish a property without individually running every case.

Do not turn that distinction into a competition in which tests become useless. Tests can expose integration problems, help explain counterexamples and check real deployment behaviour.

In the library exercise, testing several loans is useful. A proof about all permitted transitions in a precisely defined model answers a broader but also carefully bounded question. Both forms of evidence can belong in a responsible checking process.

Contents · Previous chapter · Next chapter

The library model might include available passes, allocated passes and the rules for borrowing and returning. It might leave out network messages, staff decisions and physical book movements.

That abstraction can be useful. It lets the verifier focus on a defined problem. It also establishes a boundary.

A property of the model transfers to the real system only with suitable justification that the model represents the relevant behaviour accurately enough.

The classroom analogy is a map. A map can correctly prove that one route connects two rooms in the drawing while omitting a locked door in the building. The drawing is not worthless; its usefulness depends on knowing which features it represents and which it deliberately leaves out.

Contents · Previous chapter · Next chapter

An invariant is a property intended to remain true at specified points through the model’s permitted transitions.

For the fictional pass ledger, let A mean available passes and L mean allocated passes. A proposed invariant is A + L = 3, with both quantities non-negative.

The point at which this must hold matters. Is it checked only after complete operations, at every externally observable boundary, or under some other definition?

Do not quietly switch between those meanings. A model that treats an operation as indivisible may hide intermediate behaviour visible in the actual implementation.

Writing the invariant is the beginning. The next task is to state the initial conditions and every kind of transition that could affect it.

Contents · Previous chapter · Next chapter

Suppose the ledger begins with A = 3 and L = 0. The proposed total of three holds initially.

If the real deployment instead begins with A = 3 and L = 2, a proof that assumes the first initial state does not explain the second.

This is why initialisation belongs inside the evidence boundary. A property can be preserved by every transition yet fail because the system starts outside the assumed set of states.

For beginners, check the opening line before checking the whole story. In an actual smart-contract deployment, configuration and initialisation can matter as much as the function logic. A proof about a well-initialised model does not by itself establish that the deployed instance was initialised that way.

Contents · Previous chapter · Next chapter

A simple invariant argument checks a base case and a preservation step. The base case establishes the property in the allowed starting state. The preservation step establishes that each permitted transition keeps it true.

In the pass model, borrowing one pass subtracts one from A and adds one to L, provided A is positive. Returning one reverses those changes, provided L is positive.

Under those deliberately simple rules, the sum remains three and the guards preserve non-negativity.

This is a small paper argument, not a proof of any real library contract. Its usefulness is the structure: identify a property, establish it initially, then account for every permitted way the model can change.

Contents · Previous chapter · Next chapter

The designers prove the borrowing and return rules, but forget a manager function that adds passes. Their reasoning does not cover the complete model they meant to describe.

Perhaps the addition is legitimate. If so, the total-of-three property may be the wrong requirement. Perhaps the function should be restricted. The proof cannot choose the policy for the institution.

The lesson is to enumerate the relevant transition set: ordinary actions, administrative actions, exceptional paths and changes in configuration.

A proof of two operations is evidence about those operations under its assumptions. It becomes misleading only when somebody reports it as a proof of every possible action. Keep the inventory of modelled behaviour attached to the result.

Contents · Previous chapter · Next chapter

A property might say that a successful borrowing operation preserves the total, provided the caller is authorised and at least one pass is available.

Those conditions are part of the statement. Removing them when summarising the result changes the claim.

Also ask who establishes them. If the proof assumes authorisation but the implementation never checks it, the result may not establish the access-control promise readers expected.

In the classroom, “the rule works when the teacher gives permission” is incomplete if the actual system accepts requests from anyone.

Formal reasoning can make these dependencies unusually clear. That benefit is lost if assumptions are hidden in a technical appendix while the headline announces unconditional safety.

Contents · Previous chapter · Next chapter

Suppose the statement is “whenever available passes are negative, borrowing is rejected”, while the model never permits a negative available count.

The statement can hold without exercising the intended rejection path. This kind of issue is often discussed in terms of vacuous truth.

The property may be logically correct yet unhelpful for the actual requirement.

Ask whether the relevant starting states and triggers can occur within the model. A small example trace can help explain that they are reachable.

For the pass ledger, test the meaningful boundary A = 0 rather than a forbidden state nobody can reach. A precise proof result still needs a sensible property and a meaningful connection to the behaviours users care about.

Contents · Previous chapter · Next chapter

When a verification method finds a counterexample, it provides a modelled case or sequence that violates the stated property.

Imagine a simplified faulty return rule that adds one to A but forgets to subtract one from L. Starting from A = 2 and L = 1, a return produces a total of four.

The counterexample is valuable because it locates the disagreement. It does not automatically tell us whether the implementation, specification or environment model should change.

Do not erase the failing case merely to make the checker quiet. Preserve it, understand it and compare it with the intended requirement. A failure can be a useful discovery even when it reveals a mistaken specification rather than a code defect.

Contents · Previous chapter · Next chapter

A verification tool can fail to establish a result within its supported methods or resource limits. The outcome may be unknown, timed out or otherwise incomplete.

That is different from a proof and different from a demonstrated counterexample.

A beginner interface should keep those outcomes separate. “No counterexample was reported” is not universally equivalent to “the property is proved”.

Solidity’s SMTChecker documentation distinguishes verification capabilities and limitations. The exact interpretation depends on the engine, settings and reported result.

For the library analogy, a reviewer who ran out of time has not approved the remaining pages. Respecting an incomplete result is a strength of the process, not an embarrassment to conceal behind a successful-looking dashboard.

Contents · Previous chapter · Next chapter

Some analyses examine behaviours only within a chosen bound, such as a limited number of steps. A result within that bound does not automatically establish the property for arbitrarily long execution.

Other methods can establish unbounded properties under their models. The report needs to say which kind of argument was made.

In the library exercise, checking every sequence of up to three actions is not the same claim as proving the total survives every permitted sequence.

Bounds can still be useful. They can find short failures and make a difficult problem tractable.

The mistake is not using a bound. It is dropping the bound from the conclusion. A careful summary preserves both the achievement and the conditions under which it holds.

Contents · Previous chapter · Next chapter

Our paper equation uses familiar mathematical integers. A real program may use fixed-width numbers with specific rules for overflow, underflow, division and conversion.

A proof must model the relevant semantics or justify its abstraction. An argument about unlimited mathematical integers can miss behaviour introduced by a different machine arithmetic model.

The same issue applies to units. Available passes and allocated passes are compatible quantities; kilograms and milliseconds are not.

Do not infer that all blockchain software handles arithmetic identically. Language versions and execution contexts can differ.

The beginner lesson is to ask what the symbols mean in the actual system. Mathematics is powerful because its rules are explicit; replacing those rules silently breaks the connection to the program.

Contents · Previous chapter · Next chapter

The library contract asks another component for a condition before issuing a pass. Its proof now depends on how that component behaves.

A model might assume the external component returns a truthful value, never calls back or always responds. Those assumptions may or may not describe the deployed environment.

If an assumption fails, the proof’s conclusion may no longer apply even when the prover worked correctly.

For a paper exercise, label every outside box with its assumed behaviour. Then deliberately ask what happens if it gives an unexpected answer or never answers.

This does not teach an exploit. It teaches scope: correctness of one component under a cooperative environment is not the same claim as correctness of the entire connected system under every possible environment.

Contents · Previous chapter · Next chapter

A proof concerns some identified model or implementation. Users interact with a deployed instance on a particular network.

The evidence therefore needs a connection between the proved object and the deployed code, configuration and relevant execution context.

Compiler settings, linked components and proxy implementation selection can matter. An upgrade can also change the object to which the earlier proof applied.

The fictional library keeps a proof for Manual A. If the desk starts using Manual B, the proof does not automatically follow the desk’s familiar address.

A responsible summary identifies the version and scope instead of displaying a permanent “formally verified” badge with no explanation of what was proved or which deployment it concerns.

Contents · Previous chapter · Next chapter

Suppose the pass ledger always preserves a total of three. It could still allocate every pass to the same authorised person while meeting that invariant.

The arithmetic property says nothing about fairness unless a fairness requirement is separately defined and established.

Likewise, a smart contract can satisfy its formal specification while relying on inaccurate external information or implementing a policy users dislike.

This is not an argument against proofs. It is an argument for stating the right requirements and keeping different judgments distinct.

Ask what the evidence establishes technically, what it assumes about the world and which human decisions remain outside the property. A bounded, precise claim is more useful than a grand claim whose meaning cannot be checked.

Contents · Previous chapter · Next chapter

Start with A = 3 and L = 0. Permit borrow only when A is positive; it changes the pair to A − 1 and L + 1. Permit return only when L is positive; it changes the pair to A + 1 and L − 1.

Check the initial total. Then use algebra to check the total after each permitted step. Check that the guards prevent negative values.

Now add a fictional discard operation that subtracts one from A without changing L. The original total-of-three invariant no longer fits.

Should discard be forbidden, or should the specification track a third category? That is a requirement decision. The exercise shows how proofs can reveal an incomplete account of the system rather than merely a broken calculation.

Contents · Previous chapter · Next chapter

Formal verification reasons precisely about stated properties of a defined system under stated assumptions. It can establish strong conclusions within that scope.

To read a result honestly, keep five things together: the property, the model, the assumptions, the tool’s actual outcome and the connection to the deployed object.

Proved, refuted and unresolved are different outcomes. A narrow invariant, a bounded search and a whole-system guarantee are different claims.

The useful beginner question is not “does it have a proof?” It is “what exactly was proved about which version, under which conditions, and what remains outside that statement?” Asking that question respects the value of formal methods while avoiding promises they did not make.

Contents · Previous chapter · Worked situations