Formal Methods: Just Good Engineering Practice? (2024)

It hasn’t been my experience that it is as niche as this. I believe the “costs,” people refer to in these discussions have come way down over the last couple of decades. I’ve taught developers how to use tools like TLA+ and Alloy in week.

It’s not a skill that requires a PhD and years of research to acquire these days.

Nor does writing a basic, high level specification.

If anything you will learn something about the system you are modelling by using a model checker. And that can be useful even if it is used for documentation or teaching.

The fundamental power of formal methods is that they force you to think things through.

All too often I find software developers eager to believe that they can implement concurrent algorithms armed with their own wit, a type checker, and a smattering of unit tests. It can be humbling to find errors in your design and assumptions after using a model checker. And perhaps it’s hubris that keeps programmers from using such tools in more “mundane” and “real world” contexts.

There are a lot more “small” distributed systems than you’d expect and state spaces are generally larger than you’d anticipate if you weren’t open to formalizing your work.

It’s not all or nothing!

I work on a very “product-y” back end that isn’t fully specified, but I have formally specified parts of it.

For instance, I property-based-tested a particularly nasty state machine I wrote to ensure that, no matter what kind of crazy input I called an endpoint with, the underlying state machine never made any invalid transitions. None of the code around the state machine has a formal spec, but because the state machine does, I was able to specify it.

In the process, I found some very subtle bugs I’d have never caught via traditional unit testing.

"Formal" means "written in a language that can be interpreted by a computer" and that is the very thing programmers do. Writing a code is writing a formal specification of the program's behaviour, and by definition, every piece of software must do that.

But you're right that to benefit from any formal methods, you need to compare the program's behaviour to something else that isn't the program itself, and that other thing also needs to be written in a formal language. To be able to write that other thing, you do need to have a precise understanding of what the wanted behaviour should be so that you could express it in a formal language, but it doesn't have to cover the full behaviour of the software.

As an example of what that means, take automated (unit) tests. Automated tests are a formal specification, and running them is a formal verification method. Tests are a relatively weak specification, and executing them is a relatively weak verification, compared to what we normally mean by "formal methods", but there is no clear qualitative difference -- conceptual or even practical -- between tests and more powerful formal specification and verification. You can think of these practices as more powerful tests or as tests that work differently, but tests are formal specifications, and if they're applicable to a piece of software, it's likely that richer formal specification methods are, too (learning the cost/benfit of other methods is similar to learning the cost/benefit of tests -- you don't get it right at first, but you learn along the way).

You are going to have requirements whether you like it or not. It doesn't matter if you discover them during requirements engineering and validate and deconflict them on a simple text document, or if you discover them as you go during coding (possibly after having coded the wrong thing), or if the client discovers them during the "sprint review" of some allegedly agile cult. The only difference is how much money and time are you willing to trade for being called "agile". Ironically the traditional way of doing a requirements stage is the less expensive of all three options. It is also the most aligned with the original agile spirit, since it converges with the client as soon as posible, at the point where changes are the most cheap (changing a line on a text document).

I think it's more formalisability than requiring upfront design. For example you may have an insurance claim automation system which you can't design upfront because most insurance providers have unspecified behaviour. But that doesn't mean you can refine your automation system as you get more information from interactions. You would still get the benefit that you ensure not leaving out any cases or not having any contradiction in your system

Static type checking is a kind of formal verification of software - there are formal requirements (the program doesn't go "wrong" in a number of rigorously defined ways) that are automatically checked. And you can certainly do "design and development" together in type-safe languages.

You can also use proof assistants as "unit tests" for entire classes of behaviors rather than specific values. This lets you add proofs incrementally even when a formal spec is too difficult.

I worked on a project where a couple people formally proved our design sound while I was still fixing bugs in the spec. We don’t have spherical cows. Theoretical models aren’t reality. The map is not the territory.

V&V doesn't really mean formal verification, unless you're doing some extremely cutting edge stuff. It's so much cheaper to do the basic boundary testing, fuzzing, unit & integration tests than to spend the time and find the talent who can not just formally specify but also code proofs of your requirements being met.

Formal verification is just not as common as you might think in these highly regulated industries; the expertise isn't as prevalent as your average HN reader would think.

I'm not sure that "aerospace software relies heavily on verification" is very commonly the case at all, even if one would like it to be...

Dijkstra for example didn't think so, I think. He had a din view of testing as compared with proofs for ensuring software correctness.

Everything you said about formal verification is also true about tests; do you think software is also uniquely ill suited for TDD?

That’s true. Back when they were inventing security, the requirement for high-security systems (A1 under TCSEC) required formal verification. Those who did it said its cost ranged from not too burdensome to very high. What’s the reason?

While many requirements existed, the design assurance required specifying what problem was being solved, how it’s being solved, and the safety/security properties. Then, proving that the security properties were embodied in the artifacts in all states. That problem is difficult enough that most people who succeeded were also geniuses good at programming and math. Geniuses are in short supply.

The lessons learned papers also pointed out a recurring problem. Each requirement, security policy, algorithm, etc needed a mathematical specification. Then, proof techniques were necessary that could handle each. Instead of developing software features, you are now both developing software and doing R&D on applied mathematics.

Steve Lipner’s The Ethics of Perfection pointed out it took several quarters to make a major change on a product. The markets value development velocity over quality, even demand side. So, that’s already a no go for most businesses. Likewise, the motivations of OSS developers work against high assurance practices as well.

If you want formal verification, then you are forced to make certain decisions. For one, you need to build simple systems that are easy to verify, from design to language. Then, you use the easiest, most-automated tools for the job. Most drop full verification to do automated, partial checking: TLA+, Alloy, SPARK Ada, Meta’s Infer, etc.. If doing full verification, it’s better to make or build on reusable components like we see done with CompCert and seL4. GEMSOS and VAX VMM advocated that back in the day, too.

So, most software development isn’t fit for use of formal verification. I think we can default on a combo of contracts (specs), automated testing, static analysis, and safe languages. If distributed, stronger consistency when possible. Then, use CI to run the verification on each commit. Some tools can generate patches, too.

> To use formal verification you need to have formal requirements of the behavior of your software.

Not true!

Well, it is true of TLA+, but that is why TLA+ is not the future. The future is dependent types.

It is true we'll always be programming and specifying as we go to some extent. That's why formal methods have to be part of the software itself, not some extra burden off to the side.

Dependent types is basically unique in doing that. You can right some code, then reason about that code. Or you can write a program where the propositions/proofs and executable program proper are so intertwined the separation stops making sense in theory too.

This, and this alone, supports the dialectic of "doing" and "planning" that is hardly unique to software development, but rather is emblematic of most sufficiently complex human activities.

----

A really nice example to make this concrete is Lean's standard libraries's `SatisfyingM` and `MonadSatisfying`

(See https://leanprover-community.github.io/mathlib4_docs/Batteri...)

`SatisfiesM` is an attempt to support "external" reasoning: one already wrote a non-trivial monadic action, and now one wants to do Hoare-like reasoning about preconditions, posts conditions, the returned value, etc.

But a different monadic action that uses the first one might need to then internalize this reasoning. For example, it need to turn a pair of (program, proof about program's return value) into a new program that returns the thing and the proof.

This is `MonadSatisfying` is for. It is a constraint on the monad saying we now how to internalize such a proof.

The "external" proofs are the only ones TLA+ and similar tools support, and the honest truth is that you might want to make them, you might be forced for compliance/legal/insurance reasons to make them, but you are never intrinsically forced by the software itself to make them.

The "internal proofs", in contrast, are so required. The represent different abstractions which state their interface such that it is impossible to use them incorrectly --- providing a proof is a non-negotiable obligation on user of the abstraction just as providing a "regular" argument is a non-negotiable obligation to making a regular function call.

In addition to supporting to modular reasoning --- write a very fancy thing and then make sure your coworkers don't use it incorrectly --- this fixes the economic problem --- gotta do the proofs or the code won't compile!

----

If you have no idea how to start programming more formally, here are some ways to start:

external proofs:

you probably have tests. Think, how did you know those test cases are correct? Can you rewrite individual unit tests as property tests, to "formalize" that reasoning (yes, it is still formal, even though property testing is old and simple. "formal" means "explicit" not "fancy"!). If you can write a property test to by checked by probabilistic methods, then you implicitly have a property you could proove instead. Problem solved!

internal proofs:

Does you program have any `panic("this should never happen")` or similar? Well, why shouldn't it? Types, even non-dependent ones, allow for https://en.wikipedia.org/wiki/Principle_of_explosion, which is nothing more than showing some case-alternative has been given an impossible value, and so must be dead code. Every bit of code you think is unreachable, and your intuition is not correct, has a proof saying it is in fact so, and that proof is needed internally do "discharge" the branch.

Every assert? remember "assert c = branch c -> ok; not c -> panic("this should never happen")" so all your assertions are not things you might prove!

Even people that never have written down specs in their life probably have some assertions or panics lying about. So they too have something to formalize.

IMO UML is useless because whatever diagram gets produced means different things to different people and it's very complex but not check-able so people can make UML diagrams that are self contradictory or nonsense.

I find myself using a "method" of some kind when faced with a problem that's hard to think about. A communications protocol - nice to have a state machine to describe it for example. TLA obviously fits that niche even better. I've been lucky enough not to have too many problems recently that felt like they justified that effort but it's of incredible value when one does. Domain Specific Languages - so much better to use a parser framework than hand-code if you want to avoid all sorts of undesirable outcomes.

Currently most of my rework comes from changes to the requirements and our "customers" not really knowing what they want till we give them something and they say "not that."

This is partly because the people asking for things don't fully think out all the implications of what they're asking. It's mostly about not having enough knowledge in one place to make good decisions on.

> if it was really that helpful, more people would be applying it and the benefits would speak for themselves

Well... that's not a good logic on any area, and on software development it's twice as bad.

Most software projects still fail. And that's not "market failure", it's just "didn't manage to build it".

If we’re going to boil this frog, we need to steal wisdom from TLA, not teach it. Type systems have borrowed a lot from Hinley-Milner, and are themselves a formal, partial proof.

I think I’d like to see a descendent of Property Based Testing that uses SAT or TLA techniques to rapidly condense the input space in a repeatable fashion. We should be able to deduce through parsing and code coverage that passing 12 to a function can never follow different branches than 11, but that -1 or 2^17 < n < 2^32 might.

I only am familiar with formal verification in the context of a hardware class, which is like programming but the cost:benefit is wildly different (can’t fix a physical chip after it has been fabricated very easily) and the types of designs are very different.

But, the impression I got was that the rigors of the formal verifier would sort of impose a limit on the complexity of the design just based on… completing in a reasonable timeframe and in a reasonable amount of memory space. Maybe the true victory of demanding formal verification would be fixing:

> software is big and complicated and hard to get right

By making big complex programs a pain to work with, haha.

>if it was really that helpful, more people would be applying it and the benefits would speak for themselves. They've been around a long, long time, though, and never caught on - it's hard not to conclude that there's probably a reason.

My impression is that there are actually not that many business domains where a large investment in time and money to get domain logic correctness from 98% to 99.99% correct is actually called for.

Formal methods are a large investment, too. No two ways around it.

Also, while they havent really caught on in general, some of their ideas have made it into modern type systems.

For Calculus you can easily explain to the unenlightened that many physical and engineering laws work in terms of speed and acceleration of measurable values, and Calculus is a mathematical framework for working with this.

> Maintaining a suite of proptest[1] strategies alongside the codebase is not a very much larger investment than writing unit tests by hand,

I actually generate a unit tests with LLMs a lot lately. They do a decent job and you can just ask it to be a little more exhaustive, test any edge cases it can think of, or instruct it to deal with specific ones. I know a fair bit about how to write good tests and the effort you can put in that. But LLMs can generate better tests than me way faster.

If anything, they are less likely to do a half-assed job of it than me because I tend to run out of patience doing repetitive tedious shit. This is a healthy trait to have for a software engineer: we are supposed to make stuff easier by automating it. If it feels repetitive, your reflex should be to write code to make it less repetitive. Documentation is the same. I generate that too these days and since it is so easy, I do it more often and sooner.

LLMs might trigger a minor revolution in the adoption of formal method verification. Generating a correct specification is a combination of tedious and probably relatively easy for an LLM given enough context like working code, documentation, and other hints as to what the thing should do.

I'd be a lot more likely to bother with that stuff if I can just let it generate specification and then briefly glance through them than if I have to spell everything out manually.

I think using Rust kind of signals that you care about correctness. It's compiler is probably the closest to proving your system is probably correct that you can get without resorting to formal methods. And probably a lot easier than trying to bolt on formal methods to languages that don't even use a compiler or explicitly specified types.

Yeah but proptest / qcheck is not formal methods at all. It's randomised testing.

A minor point. This is more akin to testing because you’re only checking your formulae against a subset of system traces.

Formal methods connotes comprehensive evidence about system behavior. In the case of TLA and similar system that’s a state machine and not the real system but the output for the state machine is a proof that your LTL/CTL/TLA properties hold for all behaviors of the system (traces or trees of traces).

TLA+ and the like work because they target a very small specification language.

With the large footprint of Rust, I've seen questions raised about how this will work. But haven't seen good answers.

Would love to read more.

I don’t see how the distinction makes any sense when the Verus project you linked requires you to write correctness specs. It sounded like intrinsic techniques were preferred because they would not require you to write and maintain a separate spec, but this is not the case.

Arguably, if 'real' Agile is ever found Formal Methods would be the antithesis of it: something provable and reproducible is blasphemy to True Believers.

> Get back to me when the formal methods actually generate high quality code that cannot deviate from the spec

That would be useful but there is a fundamental issue: code is too specific. İn formal specification you usually don't specify that detailed but you specify the general behaviour of the system. So usually the specification corresponds to a lot of programs with subtle differences. That's why code a documentation falls short: you don't know what is intentional and what is just a random choice. It's simply too specific to describe high level requirements.

The other way around (verification of program with respect to the specification) can be more feasible to implement.

How about https://en.wikipedia.org/wiki/SPARK_(programming_language)

Thanks, I couldn't find it via Google search on this website for some reason.

> My conclusion every time was that the code itself is the formal spec and the formal spec is the code.

Yes you can end up with tautological specs, where it's more or less a copy of the code. E.g. you aren't going to benefit much from formally verifying `max()`.

But there are many many cases where the formal specification is much much simpler and more obviously correct than the actual code. The classic examples are:

* Any kind of encoding / decoding transformation has the property `decode(encode(x)) == x`.

* Sorting: any sorting algorithm should result in a sorted array (forall i, j: i < j --> array[i] <= array[j])

This. In my very limited experience (i didn't write the code or specs), I've seen the runtime code find more bugs in the formal specs than the formal specs finding bugs in the runtime code.

I haven't done enough with Alloy to speak with any degree of competence with it, so I'll only speak on TLA+.

While I do think TLA+ is relatively easy to pick up (especially compared to Isabelle or Coq), and I think it's pretty awesome, I'm hesitant to say it's as "easy to pick up as Python". You need a basic understanding of set theory and state machines to even get started, and more advanced concepts like algorithm refinement to get into the really useful juicy stuff.

When I've tried to push TLA+ at work, the mathey syntax is usually a non-starter for most of my engineering colleagues. I don't think my coworkers are stupid by any stretch, but they are decidedly uninterested in re-learning any discrete math (if they ever learned it in the first place, which isn't a guarantee). For an engineer LARPing as an academic like me, TLA+'s notation isn't really hard at all, but I will often forget that most engineers only think in code.

Why not use python itself then? The design by contract PEP is old. Not sure if anyone is working on it.

https://adsharma.github.io/agentic-transpilers/

https://adsharma.github.io/pysmt

With most testing and verification, there's a law of diminishing returns. It helps you find stuff that you need to fix and there is always stuff to find. But at some point you've found enough of the stuff that needed fixing that you can use the software and it starts making money for you. Most people stop there. It's not going to make much more money if you continue your efforts and the risk of a lot of financial damage is usually not that high. A good software license will ensure that. You might be better off paying a decent lawyer than wasting time on formal methods. Lawyers aren't cheap. But neither is having your software engineering team faff about with a lot of complex tools for weeks on end.

And with software you can just do an update if something is found later. Not a big deal usually. There are exceptions of course. With hardware things get more expensive. But still, judging from the state of e.g. most bluetooth and other hardware I've ever owned, the barrier of good enough is pretty low there too. Mostly things work and you can usually work around minor issues when they don't.

Some, software justifies/requires going above and beyond doing testing. Especially if it controls critical hardware. I've never worked on such stuff. And even there the notion of releasing often and breaking stuff by testing it seems to be catching on. For example SpaceX is doing agile rocket development. They launch starship every few months until they get it reliable enough to launch things into orbit.

I doubt that although I agree that it's much more useful when cost of a failure is higher. For example I work in a lab that formalizes requirements and we have real customers that pay us for formalization because they find it useful. Some products are things that a failure could cause injury or even possibly death. But not all systems have that high costs and they still see benefits.