Formal methods are not one difficult, all-or-nothing practice. They are a spectrum of techniques that can provide stronger evidence about selected software properties, sometimes allowing teams to replace large numbers of tests with proof that a defined failure cannot occur.

A previous article described the 2006 Tokeneer result and the Correctness by Construction work behind it. The point was not that every software project should be built exactly that way, or that a good process can magically make software perfect. The point was that very low-defect software is possible when an organization treats defect prevention as an engineering objective rather than merely hoping that testing will find all the problems.

Most teams will have a reasonable reaction at that point. Few are developing a biometric access-control system for a national-security experiment. Few have a fixed-price high-assurance contract, a staff trained in SPARK, or a customer prepared to pay explicitly for substantial up-front rigor. Most teams have existing code, ordinary schedules, changing requirements, C or C++, and a backlog that is already growing faster than was ever thought possible.

Formal methods can sound like an impractical answer to that reality. The phrase brings to mind theorem provers, unfamiliar mathematical notation, and an expectation that every programmer must become a master logician before being allowed near a keyboard.

Some forms of formal development are demanding. They require specialized skills, careful modeling, discipline, and a willingness to find difficult design problems early, when they are still inconvenient rather than expensive. That is simply fact – for some forms.

The larger problem is that “formal methods” is often thought to mean only its most rigorous forms. This common misunderstanding can make it seem as if you need to be an academic or a dedicated specialist to gain any benefit from this remarkable family of practices.

Formal methods are tools of the mystics. They offer a range of techniques for making important software behavior precise enough to analyze rather than merely discuss.  Some “lightweight formal methods” techniques are actually built into ordinary programming languages.

What “formal” means

Formal methods use mathematically precise descriptions of some aspect of system behavior. The description might be a specification, a model, a set of contracts, a restricted programming language, or annotations attached to source code. The important point is that the behavior becomes precise enough to check, analyze, or in some cases prove.

The English language can leave room for two competent people to read the same requirement and reach different conclusions. “The controller shall shut down safely if a sensor fails” sounds clear until someone has to implement it.

Sensor failure raises several immediate questions. Does failure mean a value outside the expected range, a missing update, a value that changes too quickly, or a signal that remains plausible while being wrong? Does “safely” mean stopping immediately, entering a degraded mode, preserving the last valid output for a limited time, alerting an operator, or some combination of those actions? What happens if two sensors disagree? What happens if the shutdown mechanism itself reports a fault?

Testing will eventually expose some of those questions. A more formal approach attempts to expose them before source code, test procedures, and assumptions have all acquired momentum.

Formal methods therefore have less to do with mathematics for its own sake than with making important assumptions visible. A well-used method makes it harder for a team to proceed while a critical ambiguity remains hidden inside a requirement, an interface, or a convenient phrase such as “as appropriate.”

Useful engineering often begins there.

A spectrum of rigor

Formal methods do not occupy a single line from “easy” to “hard.” Different techniques answer different questions, cover different portions of a system, and require different kinds of investment.

A compiler warning, a coding-rule checker, and a formal proof may all identify a defect before deployment. Their evidence is not interchangeable. A compiler warning may point a reviewer toward a suspicious construction. A static-analysis tool may establish that a defined class of runtime failure cannot occur within the scope of its analysis. A proof may establish that specified properties hold for all executions covered by the formal model and its assumptions.

Precision about evidence matters because teams sometimes buy a tool, run it once, and conclude that they have “done formal methods.” A tool can be useful without providing a proof. A proof can be useful without proving that a complete delivered system meets every real-world need. Good engineering requires being exact about what evidence has actually been obtained.

The lighter end

Lightweight techniques include precise interface definitions, assertions, contracts, annotations, restricted coding rules, compiler diagnostics, and conventional static analysis. Most of these techniques are mature enough to use routinely in many development environments, including ordinary C and C++ projects.

Maturity does not mean infallibility or automation without judgment. Static-analysis tools differ greatly in the rules they apply, the language features they understand, their ability to follow data and control flow across modules, and the amount of low-value noise they produce. A tool that produces hundreds of findings that nobody considers important will eventually be ignored. The resulting failure is usually a failure to select, configure, and govern the tool properly.

Lightweight formal methods can remove certain classes of mistakes from the ordinary review burden. A tool may detect unchecked return values, use of uninitialized data, dangerous conversions, dead stores, improper resource handling, violations of defined information-flow rules, or departures from an established coding subset. None of those findings proves that the product is correct. Each one can make an avoidable defect harder to introduce and easier to find before testing begins.

Assertions and contracts offer another useful step. A precondition states what must be true when an operation is called. A postcondition states what the operation guarantees when it returns. An invariant states what must remain true while an object, data structure, or state machine is in use. Even when a contract is checked only at runtime or reviewed manually, writing it down forces a team to decide what the interface actually means.  A contract also gives static-analysis or proof tools concrete information about developer intent, and how well the implementation followed through.   Tools cannot reason meaningfully about an assumption that exists only in a programmer’s head.

An Incremental Path for C

Splint has an especially useful attribute for C projects: a team can use it at nearly any level of effort. Unannotated code can be checked for a useful set of common security and programming mistakes. Annotations can then be added where the team needs stronger checking of interfaces, ownership, nullability, global state, side effects, or other assumptions that ordinary C declarations do not express.

Splint’s ownership annotations may seem somewhat familiar to programmers who know Rust. An only reference resembles unique ownership. A dependent reference resembles a borrow from storage owned elsewhere. A temp parameter resembles a temporary borrow that a called function may use but may not retain or release.  A disciplined C project can use Splint’s memory model to prevent ownership, lifetime, and aliasing errors, gaining many of the memory safety benefits that are claimed to be exclusive to Rust. 

Full specifications can provide a stronger level of checking still. The code may be annotated or unannotated, while separate specifications describe the intended behavior of functions and interfaces in greater detail. Splint can then check the code against those specifications rather than relying solely on conventions held in the programmers’ heads.

The incremental path matters. A C team does not need to stop development, rewrite its codebase in another language, or formalize every module before obtaining a useful result. Engineers can begin by running the tool on existing code, learn what the findings reveal, add annotations to the interfaces and failure-prone areas that matter most, and extend the specifications as their understanding and needs grow.

For C programmers, Splint can be a fantastic “gateway drug” into formal methods. The first benefit may be better static checking. The larger benefit comes later, when developers discover that they can state important assumptions explicitly and ask the tool to check whether the code actually honors them.

Splint has some important caveats. The tool is more than 20 years old: its user manual dates from 2003, and the latest stable release dates from 2007. Splint is written to support ANSI C 1998 / ISO C 1999 (C99), and while it recognizes some compiler extensions, modern compiler extensions can cause problems.  Projects that rely heavily on recent language features, compiler-specific constructs, or C++ will need another tool.

Splint’s specification capability has a second practical limitation. The tool inherited LCLint’s ability to check C code against formal specifications, but the Splint guide offers little practical instruction on how to create those specifications. The older LCLint documentation is more useful for that part of the work.

Splint remains free, fast, easy to use, and exceptionally well documented for its ordinary static checks, annotations, and configuration. A C project that can remain within the tool’s language limitations can still obtain substantial value from it, beginning with unannotated code and moving toward stronger specification-based checking as the team gains experience.  While it can be used in lightweight fashion, it is also has the features to be a bona fide member of the next tier.

The middle ground

Stronger static analysis, abstract interpretation, model checking, behavioral specifications, state-machine models, and systematic use of contracts occupy the middle of the spectrum. These methods are especially useful when a team needs evidence about behavior across many possible paths rather than evidence that a selected set of test cases happened to work.

Abstract interpretation is one of the more powerful techniques in the middle of the spectrum. The name is unfamiliar to many developers, but its practical purpose is straightforward: determine what can and cannot happen in a program without having to execute every possible program run.

Abstract interpretation is one of the more powerful techniques in the middle of the spectrum. The name is unfamiliar to many developers, but its practical purpose is straightforward: reason about what can and cannot happen in a program without executing every possible program run.

A sound abstract interpreter computes a safe over-approximation of the program states that may be reached. The analysis may include some states that cannot actually occur, because including too many possible states is safer than excluding a real one. When the resulting analysis shows that no execution can reach a defined failure state, the failure has been proved impossible within the scope of the analysis.

The practical value usually lies in proving what cannot happen. A sound analysis can establish that a value cannot escape its permitted range, an array access cannot exceed its bounds, an arithmetic operation cannot overflow, an assertion failure has no reachable branch, or another defined runtime error cannot occur.

Value-range checking is one of the more practical uses of abstract interpretation. Many embedded-system failures begin with a value that is legal in the programming language but invalid in the engineering domain. A temperature may be outside the sensor’s credible range. A command may exceed an actuator limit. A conversion may produce a value that does not fit in the destination representation. A counter may wrap after a long operating interval. Range analysis can track possible values through the code and establish that a stated limit cannot be exceeded, assuming the input and environmental assumptions have been defined correctly.

Memory-bounds analysis addresses another class of failures that testing handles poorly. A test suite can exercise selected array sizes, indices, and call sequences. Sound analysis can establish that every access in the analyzed code remains within the allocated or defined bounds, including paths and input combinations that no test designer selected. For C and C++ software, that can eliminate large areas of uncertainty around array indexing, buffer handling, pointer offsets, and access through derived references.

A meaningful ASSERT can turn either kind of design claim into a concrete verification target. An assertion may state that a value remains within its allowed range, an index remains within bounds, a pointer is valid before dereference, or a state-machine transition is legal. If abstract interpretation proves that the assertion’s failure branch is unreachable, the analysis establishes that the asserted condition holds for every execution within its scope.

No ordinary test campaign provides equivalent evidence.

The underlying mathematics of abstract interpretation is sophisticated, but mature tools do not require programmers to become experts in the math. A focused course on an abstract-interpretation tool such as Polyspace can prepare experienced software engineers to configure the analysis, interpret its results, understand its assumptions and limitations, and use the results as part of a disciplined verification process in a matter of days.

The strongest end

Formal specification and deductive proof occupy the strongest end of the spectrum. A team defines required behavior precisely, establishes contracts and invariants, and develops evidence that the implementation satisfies selected properties for all executions covered by the specification, code model, and assumptions.

SPARK is a familiar example in high-integrity software. SPARK is really a subset of the Ada programming language used with a specialized set of analysis tools.  SPARK’s contracts, flow analysis, and proof tools are intended to make properties such as initialization, data dependencies, absence of specified runtime errors, and conformance to contracts amenable to analysis. The restrictions are not arbitrary inconveniences. They remove or control language behaviors that make reliable reasoning much harder.

Deductive verification has become more usable than it was when many engineers first encountered formal methods. Better automated provers, modular contracts, integrated development environments, and more practical workflows have reduced some of the clerical burden. The remaining work is still substantial. Engineers must state properties clearly, define meaningful contracts and invariants, interpret proof failures, and decide which environmental assumptions are legitimate.

A proof tool cannot rescue an incoherent requirement. A proof tool can make the incoherence harder to overlook.

Tool maturity and limits

Tool maturity should be judged by more than a product’s age or a vendor’s claims. A practical assessment includes the kinds of properties a tool checks, the language and platform coverage, the degree of automation, the quality of diagnostics, the repeatability of results, the fit with the build and review process, and the available evidence for its use in a regulated environment.

Static analysis is broadly mature as a development practice. Static-analysis tools can identify many vulnerability patterns, rule violations, and potential concurrency problems before execution. Their results still depend upon the chosen rule set, configuration, source coverage, modeling assumptions, and disciplined review of findings.

Model checking and deductive proof are mature in more focused areas. They are not universally push-button technologies, particularly for large legacy codebases, unrestricted C++, complex operating-system interactions, or systems whose essential behavior cannot be expressed clearly. NASA describes model checking as checking whether a property holds for every reachable state, while theorem proving establishes properties expressed in mathematical logic.

High-assurance work adds a separate concern: confidence in the tools themselves. A team may trust a tool enough to use it as a defect-finding aid while still requiring tests or independent reviews to establish the property being analyzed. A certification context may require a more explicit argument about the tool version, configuration, qualification evidence, and the limits of any credit claimed for its use.

Tool maturity changes the economics of formal methods. Tool maturity does not abolish engineering judgment.

Testing has a different job

Testing remains necessary to show that a system performs the correct logical behavior. A proof that a controller never exceeds a stated output limit does not establish that the selected limit is medically, physically, or operationally correct. A proof that a protocol implementation cannot deadlock does not establish that the protocol serves the customer’s actual need. A proof that a calculation cannot overflow does not establish that the calculation uses the right engineering model.

Logical correctness has to be established against requirements, expected system behavior, hardware interaction, operational scenarios, and the realities of the environment in which the software will run. Testing remains one of the principal ways to obtain that evidence.

Formal methods address a different, equally important category of question: whether defined classes of failure can occur at all.

A sound abstract interpreter can establish that important classes of implementation failure cannot occur within the analyzed scope. The most practical examples include value-range violations, arithmetic overflow or underflow, division by zero, out-of-bounds array indexing, invalid pointer arithmetic, buffer overruns, use of uninitialized data, null-pointer dereferences, resource misuse, and failure of a defined assertion. Research on aerospace software has described the automatic verification of absence of runtime errors through static analysis by abstract interpretation.

Testing samples behavior. Even very thorough testing samples selected inputs, state combinations, timing relationships, and fault conditions. A sound proof that an assertion failure is unreachable establishes that the failure branch cannot execute for any analyzed execution, including combinations that no test designer considered and combinations too numerous to enumerate economically.

A meaningful ASSERT becomes more than defensive code under that kind of analysis. The assertion becomes a precise, executable statement of a property the design must maintain. A proof that its failure branch has no reachable path establishes that the property always holds within scope.

The testing consequence is direct. Tests written solely to show that the asserted failure cannot happen may be removed or sharply reduced. The proof has established the claim more strongly than those tests could establish it.

Properties over time

Many important failures do not occur at a single line of code. They arise from sequences of events, competing tasks, timing relationships, or system states that appear individually valid but become dangerous in combination.

Deadlock is a familiar example. Each task may be well formed in isolation. Each lock acquisition may appear reasonable. The failure occurs when two or more tasks wait indefinitely for conditions that cannot be satisfied. A test suite can find a deadlock if it happens to execute the offending sequence with the relevant timing and scheduling. A model checker can examine the reachable state space and establish that no reachable state is a deadlock, subject to the accuracy and scope of the model.

Race conditions present a similar problem. A race may require a particular interleaving of tasks, interrupts, or communications. The error can disappear when logging is added, when the system runs under a debugger, or when the test environment is slightly slower than the fielded system. Tools that systematically explore interleavings can find such races, and appropriate formal tools can establish their absence within the modeled concurrency semantics.

Temporal properties extend beyond deadlock and races. A system may need to establish that a response eventually occurs after a request, that a safety action always occurs before a hazardous state is entered, that two tasks can never occupy a critical section simultaneously, that an acknowledgment cannot be accepted before the associated command is issued, or that a recovery sequence cannot be bypassed indefinitely.

Model checking is particularly well suited to such claims because it evaluates properties over possible execution paths, not merely isolated states. A property such as “a request is eventually answered” is a temporal or liveness property. A property such as “two tasks are never simultaneously in the critical section” is a safety property. Both can be expressed precisely and checked across the modeled behavior of a concurrent system.

Testing remains important after temporal properties have been verified. Testing checks whether the implementation corresponds to the model, whether actual scheduling and timing behavior match stated assumptions, whether hardware interrupts and operating-system services behave as expected, and whether the intended temporal property is the right one. Testing does not need to repeat an exhaustive search of interleavings merely to provide weaker evidence for a property already established formally.

The real value of formal methods

Formal evidence removes or reduces the need for testing where the test’s sole purpose was to establish a property that the analysis has already established more strongly.

A component might contain assertions that establish an input value remains within its permitted engineering range and that every resulting array index remains within the bounds of the data structure being accessed. A sound abstract-interpretation result can establish, before the program is ever run, that neither assertion can fail for any execution covered by the analysis. Unit tests devoted solely to demonstrating the same range and bounds properties across large numbers of ordinary, boundary, and near-boundary values no longer need to carry the evidentiary burden they otherwise would.

A verified state-machine model can provide similar relief for finite-state behavior. A model may establish that a controller cannot enter an enabled state after a defined fault condition without first completing the required recovery sequence. Tests do not need to discover every ordering of modeled state transitions merely to establish that invariant. Testing can concentrate on whether the implementation matches the model, whether real timing behaves as assumed, and whether the model omitted a relevant state or external event.

A deductive proof can establish that code satisfies a specified contract for all executions allowed by the preconditions, invariants, language semantics, and tool assumptions. Unit testing directed solely at re-demonstrating the proved contract can be reduced sharply or eliminated as verification evidence for that contract.

The following distinction is useful in planning verification work:

 

A verification plan should identify which evidence establishes each important claim. A sound proof that an assertion cannot fail should be recorded as the primary evidence for that assertion. Associated tests can then concentrate on validating assumptions, exercising integrations, checking the target environment, and exploring behavior beyond the proof boundary.

The resulting approach is not “test everything anyway, just to be safe.” Re-running weaker evidence after obtaining stronger evidence consumes time that could be used to find problems the proof did not address.

Where to begin

Teams do not need to select a grand methodology, buy a large tool suite, and retrain everybody before taking a useful step. That approach makes formal methods sound like a corporate transformation program, which is a reliable way to ensure that nothing happens.

A better starting point is one subsystem where a defect would have consequences beyond an ordinary bug report. The selected area might involve a safety decision, a security boundary, a protocol parser, a resource-ownership rule, a complex state machine, or an interface between independently developed components.

The next step is to identify several properties that must always hold. An access-control system might require that unauthorized access is never granted. A medical-device controller might require that no command sequence can drive an output beyond a defined safe limit. A financial system might require that every transfer preserves value across both normal and failure paths. A communications component might require that unvalidated external data never reaches a privileged operation.

Those statements are not complete requirements. They are structural beams in the requirements set. Once they are identified, a team can decide what form of evidence is appropriate: review, assertion, static analysis, model checking, proof, testing, or some combination.

C and C++ projects can begin with explicit interface contracts, disciplined assertions, range and unit checks, compiler diagnostics, static analysis, and annotations that express ownership or data-flow intent. Splint remains an instructive example of the underlying idea: source-code annotations can allow a tool to check assumptions that would otherwise exist only in the programmer’s head. Modern tools may be more suitable for a particular project, but the principle remains the same.

The first target should not be every warning, every module, or every possible property. The first target should be the failure modes with serious consequences and little tolerance for discovery after release.

Training has a cost

Formal methods require learning. Organizations should not pretend that a few tool licenses and a lunch presentation will produce the benefits demonstrated on high-assurance projects.

Engineers need to learn how to express properties precisely, interpret analysis results, distinguish a real defect from a modeling or annotation problem, and avoid treating tools as a replacement for judgment. Managers need to recognize that early discovery is progress, even when the discovery requires an uncomfortable redesign.

The training burden is one reason adoption has been slow. The same burden is a reason not to turn the subject into a binary choice between doing everything and doing nothing.

Many teams can gain substantial value by improving precision at interfaces, in critical state logic, and along consequential failure paths. Some systems justify much stronger methods. Others do not. Good engineering requires making that distinction honestly.

The cost argument should also include the full cost of the decision. Up-front specification, analysis, review, training, and proof are visible and budgeted. Defects found late arrive as schedule disruption, emergency releases, field support, operational recovery, customer dissatisfaction, security exposure, regulatory attention, and exhausted engineers trying to repair a system while it remains in service.

Prevention is not free, but neither is failure.

More precision, less mystique

Correctness by Construction remains a striking example of what can be achieved when an organization commits to high rigor from the beginning. That doesn’t suggest that every project must duplicate the Praxis process in full.  The practical lesson is that formality is available in degrees.

Each time a team makes a critical behavior more precise, makes an assumption visible, constrains a dangerous implementation choice, or checks an important property automatically, part of the system moves out of the realm of hope and into the realm of evidence.

Formal methods do not make testing obsolete. Formal methods give testing a more appropriate job.

Testing establishes that the system implements the right logic, interacts correctly with the real world, meets its operational needs, and fulfills requirements that may themselves have been incomplete or wrong. Formal methods can establish that some classes of failure do not exist: an assertion cannot fail, a value cannot escape its defined range, a buffer access cannot exceed its bounds, an overflow cannot occur, a forbidden state cannot be reached, a race cannot arise within the modeled concurrency semantics, a deadlock cannot occur, or a required response cannot be postponed indefinitely.

The engineering advantage is substantial. A team does not need to spend its test budget repeatedly sampling failure modes that a suitable formal method has already ruled out. The recovered effort can be directed toward requirements, system integration, hardware, timing, environmental faults, operational scenarios, and the awkward realities that remain outside the formal boundary.

The practical objective is not formal proof everywhere. The practical objective is to use the strongest reasonable evidence where the consequences justify it, then direct testing toward assumptions, integrations, operating conditions, and human realities that no mathematical treatment has settled.

Learn More

Engineering the Tokeneer Enclave Protection Software

Tokeneer: Beyond Formal Program Verification

Introduction to Formal Verification with SPARK

NIST: Recommended Minimum Standards for Vendor or Developer Verification of Code

Splint