11 ms·

Systems Correctness Practices at Amazon Web Services

383 points by tanelpoder 1y ago

agentultra 1y ago
What’s been disappointing to me is how easily formal methods are dismissed in industry. TLA takes some time to learn to wield effectively but it pays off on spades.
- deleted 1y ago
  [deleted]
EGreg 1y ago
Wow. I used to correspond with Leslie Lamport years ago (about his Buridan's Principle papers, etc.) Today I went to his website and discovered a lot about TLA+ and PlusCal. He still maintains it: https://lamport.azurewebsites.net/tla/peterson.html?back-link=high-level-view.html https://lamport.azurewebsites.net/tla/peterson.html?back-lin... I must say ... it would make total sense for a guy like that, who brought mathematics to programming and was an OG of concurrent systems, to create a systems design language that's used at AWS and other industrial places that need to serve people. I wish more people who build distributed systems would use what he made. Proving correctness is crucial in large systems.
- lopatin 1y ago
  And just a tip for who may be intersted: Claude Opus with Extended Thinking seems to be very good at converting existing code into TLA+ specs. I've found multiple bugs for personal Rust projects like this (A Snake game that allowed a snake to do a 180 degree turn), and have verified some small core C++ components at work with it as well (a queue that has certain properties around locking and liveness). I tried other models but kept getting issues with syntax and spec logic with anything else besides Opus.
  - dosnem 1y ago
    I’ve always envisioned tla and other formal methods as specific to distributed systems and never needed to understand it. How is it used for a snake game? Also how is the TLA+ spec determined from the code? Won’t it implicitly model incorrect bugs as correct behaviour since it’s an existing state in the system? Also when using TLA from the start, can it be applied to implementations? Or is it only for catching bugs during design? Therefore I’m assuming implementations still need to match the design exactly or else you would still get subtle bugs? Sorry for all the questions I’ve never actually learned formal methods but have always been interested.
    - lopatin 1y ago
      Here's how it caught my Snake bug: My snake representation is a vector of key points (head, turns, tail). A snake in a straight line, of length 3, facing right can look like this: [(0,0), (2,0)]. When a Snake moves (a single function called "step_forward"), the Snake representation is compressed by my code: If the last 2 points are the same, remove the last one. So if this snake changes direction to "left", then the new snake representation would be [(1, 1), (1, 1)] and compressed to [(1, 1)] before existing out of step_forward. Here's how the bug was caught: It should be impossible for the Snake representation to be < 2 points. So I told Opus to model the behavior of my snake, and also to write a TLA+ invariant that the snake length should never be under 2. TLA+ then basically simulates it and finds the exact sequence of steps "turns" that cause that invariant to not hold. In this case it was quite trivial, I never thought to prevent a Snake from making turns that are not 90 degrees.
    - Jtsummers 1y ago
      It's targeted at distributed systems, but it can be used to model any system over time. I've used it for distributed systems, but also for embedded systems with a peculiar piece of hardware that (seemed, and we found was) to be misbehaving. I modeled the hardware and its spec in TLA+, then made changes to the behavior description to see if it broke any expected invariants (it did, in precisely the way we saw with the real hardware). The TLA+ model also helped me develop better reproducible test cases for that hardware compared to what we were doing before.
- skydhash 1y ago
  > Proving correctness is crucial in large systems. It could be good in smaller, but critical and widely used utilities like SSH and terminals.
  - oblio 1y ago
    Yeah, basically all the coreutils plus all the common extras (rsync, ssh, etc) could use stuff like this.
    - rthnbgrredf 1y ago
      It should be feasible to rewrite the coreitils like ls, cd and cp in Lean 4 together with Cursor within days. Rsync and ssh are more complex though.
      - oblio 1y ago
        Your first claim is actually a very solid test for AI. We should start seeing a lot more AI powered OSS projects or at least contributions if AI truly is as good as they say. Heck, OSS should accelerate exponentially since contributions should become very easy.
- belter 1y ago
  >> Proving correctness is crucial in large systems. You can't do that... The model checker says the specification satisfies the properties you wrote within the finite state space you explored...
  - amw-zero 1y ago
    You can write proofs in TLA+ and many other formalisms. You don’t need to ever use a model checker. The proofs hold for an infinite number of infinite-length executions. We are definitely not limited to finite behaviors.
sebstefan 1y ago
>Deterministic simulation. Another lightweight method widely used at AWS is deterministic simulation testing, in which a distributed system is executed on a single-threaded simulator with control over all sources of randomness, such as thread scheduling, timing, and message delivery order. Tests are then written for particular failure or success scenarios, such as the failure of a participant at a particular stage in a distributed protocol. The nondeterminism in the system is controlled by the test framework, allowing developers to specify orderings they believe are interesting (such as ones that have caused bugs in the past). The scheduler in the testing framework can also be extended for fuzzing of orderings or exploring all possible orderings to be tested. This is fucking amazing
- jeffreygoesto 1y ago
  Loom for Rust does this. We also adapted it for some C++ with good success (found actual bugs that slipped tests and reviewes). Sits lower than i.e. TLA+ and is not a proof but super useful as you check the actual implementation. https://github.com/tokio-rs/loom https://github.com/tokio-rs/loom
- deleted 1y ago
  [deleted]
- agentultra 1y ago
  The TigerBeetle team does this too and it's an interesting approach. One of their developers did a talk on it at HYTRADBOI this year [0]. [0] https://www.hytradboi.com/2025/c222d11a-6f4d-4211-a243-f5b7fafc8d79-rocket-science-of-simulation-testing https://www.hytradboi.com/2025/c222d11a-6f4d-4211-a243-f5b7f...
  - slt2021 1y ago
    they also made a browser game to showcase their DST, where you can inject faults and see how tigerbeetle recovers https://sim.tigerbeetle.com/ https://sim.tigerbeetle.com/
    - 1y ago
mlhpdx 1y ago
> 92% of catastrophic failures in tested distributed systems were triggered by incorrect handling of nonfatal errors This. If you take nothing else away from the article (which has a lot) take this: fail well, don’t fail poorly.
- deleted 1y ago
  [deleted]
- senthil_rajasek 1y ago
  It would also be nice to list some "best practices" on how to handle non-fatal errors. I would be definitely interested to know of any sources.
  - skydhash 1y ago
    The same way you handle fatal errors, by specifying the exceptional circumstances and how to handle them (retry, alternative actions, or signaling to another handler up the call/request tree). Something’s correct output may not be our thing’s correct input.
  - harrall 1y ago
    I think the best practice is to handle them with equal attention as the happy path. Error handling is usually afterthought from my experience. What is the system state when it does error? What is the best possible recovery from each error state? What can the user/caller expect for an error?
  - hiddencost 1y ago
    One I see a lot is not being careful to use the correct error type / status code. E.g. if you're in python and raise a value error when an API is rate limited, someone down stream from you is going to have a bad time.
  - jerf 1y ago
    One of the nice things about "errors as values" is that it is generally easier to shim in an error rather than shim in an exception. Not that it's impossible to do the latter, but it's just generally easier because you can have that error serving as a value in your test code. I have a lot of Go testing shims that look like: type UserGetter interface { GetUser(userID string) (User, error) } type TestUsers struct { Users map[string]User Error error } func (t TestUsers) GetUser(userID string) (User, error) { if t.Error != nil { return User{}, t.Error } user, have := t.Users[userID] if !have { return User{}, ErrUserNotFound } return user, nil } This allows easily testing errors upon retrieving users and ensuring the correct thing happens. I'm not a 100% maniacal "get 100% test coverage in everything" kind of guy, but on the flip side, if your test coverage only lights up the "happy path", your testing is not good enough and as you scale up the probability that your system is going to do something very wrong when an error occurs very rapidly approaches 1. It's more complicated when you have something like a byte stream where you want to simulate a failure at arbitrary points in the stream, but similar techniques can get you as close as you like, depending on how close that is. From there, in terms of "how do you handle non-fatal errors", there really isn't a snap rule to give. Quite often you just propagate because there isn't anything else to do. Sometimes you retry some bounded number of times, maybe with backoff. Sometimes you log things and move on. Sometimes you have a fallback you may try. It just depends on your needs. I write a lot of network code, and I find that once my systems mature it's actually the case that rather a lot of the errors in the system get some sort of handling beyond "just propagate it up", but it's hard for me to ever guess in advance what they will be. It's a lot easy to mentally design all the happy paths than it is to figure out all the ways the perverse external universe will screw them up and how we can try to mitigate the issues.
ctkhn 1y ago
This sounds interesting but as someone who hasn't worked at AWS, and isn't already familiar with TLA+ or P, I would have liked to see even a hello world example of either of them. Without that, it sounds like a lot of extra pain for things that a good design and testing process should catch anyway. Seeing a basic example in the article itself that would give me a better insight into what these actually do.
- dmd 1y ago
  The entire point of using formal methods is that testing will never, ever catch everything.
  - nickpsecurity 1y ago
    Whereas, formal verification only catches what properties one correctly specifies in what portions of the program one correctly specifies. In many, there's a gap between these and correctness of the real-world code. Some projects closed that gap but most won't.
    - hamburglar 1y ago
      We should have formal verification of the formal verification specification. Standing on a turtle.
      - Twisol 1y ago
        I've heard that called "validation". In other words, you verify that your solution meets the problem specification, but you validate that your specification is actually what you need.
      - nickpsecurity 1y ago
        You're looking for foundational, proof-carrying code with verified logins. I can't find the verified logic right now, though. Examples: https://www.cs.princeton.edu/~appel/papers/fpcc.pdf https://www.cs.princeton.edu/~appel/papers/fpcc.pdf https://hol-light.github.io/ https://hol-light.github.io/ I'll also add that mutation testing has found specification errors, too. https://github.com/EngineeringSoftware/mcoq https://github.com/EngineeringSoftware/mcoq
vaxman 1y ago
[flagged]
hakhak 1y ago
[flagged]
amazingamazing 1y ago
> Deterministic simulation. Another lightweight method widely used at AWS is deterministic simulation testing, in which a distributed system is executed on a single-threaded simulator with control over all sources of randomness, such as thread scheduling, timing, and message delivery order. Tests are then written for particular failure or success scenarios, such as the failure of a participant at a particular stage in a distributed protocol. The nondeterminism in the system is controlled by the test framework, allowing developers to specify orderings they believe are interesting (such as ones that have caused bugs in the past). The scheduler in the testing framework can also be extended for fuzzing of orderings or exploring all possible orderings to be tested. Any good open source libraries that do this that are language agnostic? Seems doable - spin up a container with some tools within it. Said tools require some middleware to know when a test is going to be run, when test is run, tools basically make certain things, networking, storage, etc "determinstic" in the context of the test run. This is more-or-less what antithesis does, but haven't seen anything open source yet. You of course, could write your tests well, such that you can stub out I/O, but that's work and not everyone will write their tests well anyway (you should do this anyway, but it's nicer imo if this determinism is on a layer higher than the application). as a slight sidebar - I'm not really bullish on AI, but I think testing is one of the things where AI will hopefully shine, because the feedback loop during prompting can be driven by your actual application requirements, such that the test implementation (driven by AI), requirements (driven by you as the prompt) and "world" (driven by the actual code being tested) can hopefully help drive all three to some theoretical ideal. if AI gives us anything, I'm hoping it can make software a more rigorous discipline by making formal verification more doable.
- wwilson 1y ago
  There have historically been two giant adoption challenges for DST. (1) Previously, you had to build your entire system around one of the simulation frameworks (and then not take any dependencies). (2) It’s way too easy to fool yourself with weak search/input generation, which makes all your tests look green when actually you aren’t testing anything nontrivial. As you say, Antithesis is trying to solve both of these problems, but they are very challenging. I don’t know of anybody else who has a reliable way of retrofitting determinism onto arbitrary software. Facebook’s Hermit project tried to do this with a deterministic Linux userspace, but is abandoned. (We actually tried the same thing before we wrote our hypervisor, but found it didn’t work well). A deterministic computer is a generically useful technology primitive beyond just testing. I’m sure somebody else will create one someday, or we will open-source ours.
chubot 1y ago
One thing I wondered about the P language: It seems like in the early days, it was used at Microsoft to generate C code that’s actually used at runtime in the Windows USB stack? But now it is no longer used to generate production code? I asked that question here, which I think was the same question as in a talk: https://news.ycombinator.com/item?id=34284557 https://news.ycombinator.com/item?id=34284557 It seems like if the generated code is used in a kernel, it could also be used in a cloud, which is less resource-constrained
- algorithmsRcool 1y ago
  It looks like Coyote[0], which is used in azure, was an evolution of P# which was an evolution of P [0]https://www.microsoft.com/en-us/research/wp-content/uploads/2021/09/poolmanager-coyote.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/...
  - inaseer 1y ago
    +1. We have used Coyote/P# not just for model checking an abstract design (which no doubt is very useful) but testing real implementations of production services at Microsoft.
    - k__ 1y ago
      How do Coyote and P differ?
    - chubot 1y ago
      OK, but then not for generating production code? I thought I read that somewhere, but now I can't find the claim
furkansahin 1y ago
Amazing article! Using state machines is a must if you are building infrastructure control-planes. Was P a must, though? I am not sure. We have been building infrastructure control-planes for over 13 years now and every iteration we have built with Ruby. It worked wonders for us https://www.ubicloud.com/blog/building-infrastructure-control-planes-in-ruby https://www.ubicloud.com/blog/building-infrastructure-contro...
ahalbert4 1y ago
Just curious, has anyone used FIS in their own distributed services? I'm considering using it but don't have any real word experience handling those kind of experiments.
severusdd 1y ago
The 92 % stat looks really interesting! It’s rarely the spectacular crash that knocks a cluster over. Instead, the “harmless” retry leaks state until everything breaks at 2 a.m on one fateful Friday. Evidently, we should budget more engineering hours for mediocre, silent failures than for outright disasters. That’s where the bodies are buried.
- smallnix 1y ago
  Or survivorship bias: the major issues, that have been addressed, do not cause problems cause they were addressed. Some of the minor issues that are not addressed randomly do cause major issues.
Marazan 1y ago
Would I be right in saying Promela and SPIN are at a higher level than what is being described in the article?
- mjb 1y ago
  I (one of the authors) did some distributed systems work with Promela about a decade ago, but it never felt like the right fit in the domain. It's got some cool ideas, and may be worth revisiting at some point.
simonw 1y ago
S3 remains one of the most amazing pieces of software I've ever seen. That thing a few years ago where they just added strong read-after-write consistency to the whole system? Incredible software engineering. https://aws.amazon.com/blogs/aws/amazon-s3-update-strong-read-after-write-consistency/ https://aws.amazon.com/blogs/aws/amazon-s3-update-strong-rea...
- positisop 1y ago
  Google Cloud Storage had it for eons before S3. GCS comes across as a much better thought-out and built product.
  - throitallaway 1y ago
    From my POV Amazon designs its services from a "trust nothing, prepare for the worst case" perspective. Eventual consistency included. Sometimes that's useful and most of the time it's a PITA.
  - SteveNuts 1y ago
    Sure, but whose (compatible) API is GCS using again? Also keep in mind that S3 is creeping up on 20 years old, so backing a change in like that is incredible.
    - benoau 1y ago
      Not just 20 years old - an almost flawless 20 years at massive scale.
      - SteveNuts 1y ago
        It's funny that things that are pinnacles of human engineering exist like this where the general public has no idea it even exists, though they (most likely) use it every single day.
        ninetyninenine 1y ago
abeppu 1y ago
> to more lightweight semi-formal approaches (such as property-based testing, fuzzing, and runtime monitoring) Ok, I get how property-based testing and fuzzing have a relationship to formal methods (the thing being checked looks like part of a formal specification, and in some sense these are a subset of the checks that a model-checking confirms), but calling runtime monitoring a "semi-formal approach" seems like a real stretch.
- mjb 1y ago
  Runtime monitoring with something like PObserve is a semi-formal approach. Not just regular alarming and metrics.
hipgoat 1y ago
It a comment of assesment
purpleidea 1y ago
It's very interesting (I applaud this) that one of the main goals seems to be to make it more approachable as compared to TLA+, but then they go in write it in C# which I consider to be an incredibly unapproachable community and language. I'm not trying to draw the ire of the Microsoft fan boys, and there are certainly smart people working on that, but it's just not going to happen for most people. Had this been in golang, or maybe java, I'm sure many more hands would be digging in! Having said that, I hope this helps bring correctness and validation more into the mainstream. I've been casually following the project for a while now. My long-term goal is to integrate model validation into https://github.com/purpleidea/mgmt/ https://github.com/purpleidea/mgmt/ so if this is an area of interest to you, please let me know!
sylware 1y ago
Hopefully, they have now a reactive security team, because I do not count the harcking bots/ip scanners they are protecting on their "cloud".
osigurdson 1y ago
It is interesting how the industry ended up with things like TDD when it doesn't work for something as simple as a function that adds two numbers together. While not completely useless in some edge cases, its complete lack of any kind of formal underpinnings should have given us a clue. So many bad / unexamined ideas in the Uncle Bob era. Far closer to a religion than anything else (complete with process "rituals" even).

383 points by tanelpoder 1y ago

What’s been disappointing to me is how easily formal methods are dismissed in industry. TLA takes some time to learn to wield effectively but it pays off on spades.

deleted 1y ago
[deleted]

EGreg 1y ago

Wow. I used to correspond with Leslie Lamport years ago (about his Buridan's Principle papers, etc.) Today I went to his website and discovered a lot about TLA+ and PlusCal. He still maintains it: https://lamport.azurewebsites.net/tla/peterson.html?back-link=high-level-view.html https://lamport.azurewebsites.net/tla/peterson.html?back-lin... I must say ... it would make total sense for a guy like that, who brought mathematics to programming and was an OG of concurrent systems, to create a systems design language that's used at AWS and other industrial places that need to serve people. I wish more people who build distributed systems would use what he made. Proving correctness is crucial in large systems.

lopatin 1y ago
And just a tip for who may be intersted: Claude Opus with Extended Thinking seems to be very good at converting existing code into TLA+ specs. I've found multiple bugs for personal Rust projects like this (A Snake game that allowed a snake to do a 180 degree turn), and have verified some small core C++ components at work with it as well (a queue that has certain properties around locking and liveness). I tried other models but kept getting issues with syntax and spec logic with anything else besides Opus.
- dosnem 1y ago
  I’ve always envisioned tla and other formal methods as specific to distributed systems and never needed to understand it. How is it used for a snake game? Also how is the TLA+ spec determined from the code? Won’t it implicitly model incorrect bugs as correct behaviour since it’s an existing state in the system? Also when using TLA from the start, can it be applied to implementations? Or is it only for catching bugs during design? Therefore I’m assuming implementations still need to match the design exactly or else you would still get subtle bugs? Sorry for all the questions I’ve never actually learned formal methods but have always been interested.
  - lopatin 1y ago
    Here's how it caught my Snake bug: My snake representation is a vector of key points (head, turns, tail). A snake in a straight line, of length 3, facing right can look like this: [(0,0), (2,0)]. When a Snake moves (a single function called "step_forward"), the Snake representation is compressed by my code: If the last 2 points are the same, remove the last one. So if this snake changes direction to "left", then the new snake representation would be [(1, 1), (1, 1)] and compressed to [(1, 1)] before existing out of step_forward. Here's how the bug was caught: It should be impossible for the Snake representation to be < 2 points. So I told Opus to model the behavior of my snake, and also to write a TLA+ invariant that the snake length should never be under 2. TLA+ then basically simulates it and finds the exact sequence of steps "turns" that cause that invariant to not hold. In this case it was quite trivial, I never thought to prevent a Snake from making turns that are not 90 degrees.
  - Jtsummers 1y ago
    It's targeted at distributed systems, but it can be used to model any system over time. I've used it for distributed systems, but also for embedded systems with a peculiar piece of hardware that (seemed, and we found was) to be misbehaving. I modeled the hardware and its spec in TLA+, then made changes to the behavior description to see if it broke any expected invariants (it did, in precisely the way we saw with the real hardware). The TLA+ model also helped me develop better reproducible test cases for that hardware compared to what we were doing before.
skydhash 1y ago
> Proving correctness is crucial in large systems. It could be good in smaller, but critical and widely used utilities like SSH and terminals.
- oblio 1y ago
  Yeah, basically all the coreutils plus all the common extras (rsync, ssh, etc) could use stuff like this.
  - rthnbgrredf 1y ago
    It should be feasible to rewrite the coreitils like ls, cd and cp in Lean 4 together with Cursor within days. Rsync and ssh are more complex though.
    - oblio 1y ago
      Your first claim is actually a very solid test for AI. We should start seeing a lot more AI powered OSS projects or at least contributions if AI truly is as good as they say. Heck, OSS should accelerate exponentially since contributions should become very easy.
belter 1y ago
>> Proving correctness is crucial in large systems. You can't do that... The model checker says the specification satisfies the properties you wrote within the finite state space you explored...
- amw-zero 1y ago
  You can write proofs in TLA+ and many other formalisms. You don’t need to ever use a model checker. The proofs hold for an infinite number of infinite-length executions. We are definitely not limited to finite behaviors.

sebstefan 1y ago

jeffreygoesto 1y ago
Loom for Rust does this. We also adapted it for some C++ with good success (found actual bugs that slipped tests and reviewes). Sits lower than i.e. TLA+ and is not a proof but super useful as you check the actual implementation. https://github.com/tokio-rs/loom https://github.com/tokio-rs/loom
deleted 1y ago
[deleted]
agentultra 1y ago
The TigerBeetle team does this too and it's an interesting approach. One of their developers did a talk on it at HYTRADBOI this year [0]. [0] https://www.hytradboi.com/2025/c222d11a-6f4d-4211-a243-f5b7fafc8d79-rocket-science-of-simulation-testing https://www.hytradboi.com/2025/c222d11a-6f4d-4211-a243-f5b7f...
- slt2021 1y ago
  they also made a browser game to showcase their DST, where you can inject faults and see how tigerbeetle recovers https://sim.tigerbeetle.com/ https://sim.tigerbeetle.com/
  - 1y ago

mlhpdx 1y ago

> 92% of catastrophic failures in tested distributed systems were triggered by incorrect handling of nonfatal errors This. If you take nothing else away from the article (which has a lot) take this: fail well, don’t fail poorly.

deleted 1y ago
[deleted]
senthil_rajasek 1y ago
It would also be nice to list some "best practices" on how to handle non-fatal errors. I would be definitely interested to know of any sources.
- skydhash 1y ago
  The same way you handle fatal errors, by specifying the exceptional circumstances and how to handle them (retry, alternative actions, or signaling to another handler up the call/request tree). Something’s correct output may not be our thing’s correct input.
- harrall 1y ago
  I think the best practice is to handle them with equal attention as the happy path. Error handling is usually afterthought from my experience. What is the system state when it does error? What is the best possible recovery from each error state? What can the user/caller expect for an error?
- hiddencost 1y ago
  One I see a lot is not being careful to use the correct error type / status code. E.g. if you're in python and raise a value error when an API is rate limited, someone down stream from you is going to have a bad time.
- jerf 1y ago
  One of the nice things about "errors as values" is that it is generally easier to shim in an error rather than shim in an exception. Not that it's impossible to do the latter, but it's just generally easier because you can have that error serving as a value in your test code. I have a lot of Go testing shims that look like: type UserGetter interface { GetUser(userID string) (User, error) } type TestUsers struct { Users map[string]User Error error } func (t TestUsers) GetUser(userID string) (User, error) { if t.Error != nil { return User{}, t.Error } user, have := t.Users[userID] if !have { return User{}, ErrUserNotFound } return user, nil } This allows easily testing errors upon retrieving users and ensuring the correct thing happens. I'm not a 100% maniacal "get 100% test coverage in everything" kind of guy, but on the flip side, if your test coverage only lights up the "happy path", your testing is not good enough and as you scale up the probability that your system is going to do something very wrong when an error occurs very rapidly approaches 1. It's more complicated when you have something like a byte stream where you want to simulate a failure at arbitrary points in the stream, but similar techniques can get you as close as you like, depending on how close that is. From there, in terms of "how do you handle non-fatal errors", there really isn't a snap rule to give. Quite often you just propagate because there isn't anything else to do. Sometimes you retry some bounded number of times, maybe with backoff. Sometimes you log things and move on. Sometimes you have a fallback you may try. It just depends on your needs. I write a lot of network code, and I find that once my systems mature it's actually the case that rather a lot of the errors in the system get some sort of handling beyond "just propagate it up", but it's hard for me to ever guess in advance what they will be. It's a lot easy to mentally design all the happy paths than it is to figure out all the ways the perverse external universe will screw them up and how we can try to mitigate the issues.

ctkhn 1y ago

This sounds interesting but as someone who hasn't worked at AWS, and isn't already familiar with TLA+ or P, I would have liked to see even a hello world example of either of them. Without that, it sounds like a lot of extra pain for things that a good design and testing process should catch anyway. Seeing a basic example in the article itself that would give me a better insight into what these actually do.

dmd 1y ago
The entire point of using formal methods is that testing will never, ever catch everything.
- nickpsecurity 1y ago
  Whereas, formal verification only catches what properties one correctly specifies in what portions of the program one correctly specifies. In many, there's a gap between these and correctness of the real-world code. Some projects closed that gap but most won't.
  - hamburglar 1y ago
    We should have formal verification of the formal verification specification. Standing on a turtle.
    - Twisol 1y ago
      I've heard that called "validation". In other words, you verify that your solution meets the problem specification, but you validate that your specification is actually what you need.
    - nickpsecurity 1y ago
      You're looking for foundational, proof-carrying code with verified logins. I can't find the verified logic right now, though. Examples: https://www.cs.princeton.edu/~appel/papers/fpcc.pdf https://www.cs.princeton.edu/~appel/papers/fpcc.pdf https://hol-light.github.io/ https://hol-light.github.io/ I'll also add that mutation testing has found specification errors, too. https://github.com/EngineeringSoftware/mcoq https://github.com/EngineeringSoftware/mcoq

vaxman 1y ago

[flagged]

hakhak 1y ago

[flagged]

amazingamazing 1y ago

> Deterministic simulation. Another lightweight method widely used at AWS is deterministic simulation testing, in which a distributed system is executed on a single-threaded simulator with control over all sources of randomness, such as thread scheduling, timing, and message delivery order. Tests are then written for particular failure or success scenarios, such as the failure of a participant at a particular stage in a distributed protocol. The nondeterminism in the system is controlled by the test framework, allowing developers to specify orderings they believe are interesting (such as ones that have caused bugs in the past). The scheduler in the testing framework can also be extended for fuzzing of orderings or exploring all possible orderings to be tested. Any good open source libraries that do this that are language agnostic? Seems doable - spin up a container with some tools within it. Said tools require some middleware to know when a test is going to be run, when test is run, tools basically make certain things, networking, storage, etc "determinstic" in the context of the test run. This is more-or-less what antithesis does, but haven't seen anything open source yet. You of course, could write your tests well, such that you can stub out I/O, but that's work and not everyone will write their tests well anyway (you should do this anyway, but it's nicer imo if this determinism is on a layer higher than the application). as a slight sidebar - I'm not really bullish on AI, but I think testing is one of the things where AI will hopefully shine, because the feedback loop during prompting can be driven by your actual application requirements, such that the test implementation (driven by AI), requirements (driven by you as the prompt) and "world" (driven by the actual code being tested) can hopefully help drive all three to some theoretical ideal. if AI gives us anything, I'm hoping it can make software a more rigorous discipline by making formal verification more doable.

wwilson 1y ago
There have historically been two giant adoption challenges for DST. (1) Previously, you had to build your entire system around one of the simulation frameworks (and then not take any dependencies). (2) It’s way too easy to fool yourself with weak search/input generation, which makes all your tests look green when actually you aren’t testing anything nontrivial. As you say, Antithesis is trying to solve both of these problems, but they are very challenging. I don’t know of anybody else who has a reliable way of retrofitting determinism onto arbitrary software. Facebook’s Hermit project tried to do this with a deterministic Linux userspace, but is abandoned. (We actually tried the same thing before we wrote our hypervisor, but found it didn’t work well). A deterministic computer is a generically useful technology primitive beyond just testing. I’m sure somebody else will create one someday, or we will open-source ours.

chubot 1y ago

One thing I wondered about the P language: It seems like in the early days, it was used at Microsoft to generate C code that’s actually used at runtime in the Windows USB stack? But now it is no longer used to generate production code? I asked that question here, which I think was the same question as in a talk: https://news.ycombinator.com/item?id=34284557 https://news.ycombinator.com/item?id=34284557 It seems like if the generated code is used in a kernel, it could also be used in a cloud, which is less resource-constrained

algorithmsRcool 1y ago
It looks like Coyote[0], which is used in azure, was an evolution of P# which was an evolution of P [0]https://www.microsoft.com/en-us/research/wp-content/uploads/2021/09/poolmanager-coyote.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/...
- inaseer 1y ago
  +1. We have used Coyote/P# not just for model checking an abstract design (which no doubt is very useful) but testing real implementations of production services at Microsoft.
  - k__ 1y ago
    How do Coyote and P differ?
  - chubot 1y ago
    OK, but then not for generating production code? I thought I read that somewhere, but now I can't find the claim

furkansahin 1y ago

Amazing article! Using state machines is a must if you are building infrastructure control-planes. Was P a must, though? I am not sure. We have been building infrastructure control-planes for over 13 years now and every iteration we have built with Ruby. It worked wonders for us https://www.ubicloud.com/blog/building-infrastructure-control-planes-in-ruby https://www.ubicloud.com/blog/building-infrastructure-contro...

ahalbert4 1y ago

Just curious, has anyone used FIS in their own distributed services? I'm considering using it but don't have any real word experience handling those kind of experiments.

severusdd 1y ago

The 92 % stat looks really interesting! It’s rarely the spectacular crash that knocks a cluster over. Instead, the “harmless” retry leaks state until everything breaks at 2 a.m on one fateful Friday. Evidently, we should budget more engineering hours for mediocre, silent failures than for outright disasters. That’s where the bodies are buried.

smallnix 1y ago
Or survivorship bias: the major issues, that have been addressed, do not cause problems cause they were addressed. Some of the minor issues that are not addressed randomly do cause major issues.

Marazan 1y ago

Would I be right in saying Promela and SPIN are at a higher level than what is being described in the article?

mjb 1y ago
I (one of the authors) did some distributed systems work with Promela about a decade ago, but it never felt like the right fit in the domain. It's got some cool ideas, and may be worth revisiting at some point.

simonw 1y ago

S3 remains one of the most amazing pieces of software I've ever seen. That thing a few years ago where they just added strong read-after-write consistency to the whole system? Incredible software engineering. https://aws.amazon.com/blogs/aws/amazon-s3-update-strong-read-after-write-consistency/ https://aws.amazon.com/blogs/aws/amazon-s3-update-strong-rea...

positisop 1y ago
Google Cloud Storage had it for eons before S3. GCS comes across as a much better thought-out and built product.
- throitallaway 1y ago
  From my POV Amazon designs its services from a "trust nothing, prepare for the worst case" perspective. Eventual consistency included. Sometimes that's useful and most of the time it's a PITA.
- SteveNuts 1y ago
  Sure, but whose (compatible) API is GCS using again? Also keep in mind that S3 is creeping up on 20 years old, so backing a change in like that is incredible.
  - benoau 1y ago
    Not just 20 years old - an almost flawless 20 years at massive scale.
    - SteveNuts 1y ago
      It's funny that things that are pinnacles of human engineering exist like this where the general public has no idea it even exists, though they (most likely) use it every single day.
      - ninetyninenine 1y ago

abeppu 1y ago

> to more lightweight semi-formal approaches (such as property-based testing, fuzzing, and runtime monitoring) Ok, I get how property-based testing and fuzzing have a relationship to formal methods (the thing being checked looks like part of a formal specification, and in some sense these are a subset of the checks that a model-checking confirms), but calling runtime monitoring a "semi-formal approach" seems like a real stretch.

mjb 1y ago
Runtime monitoring with something like PObserve is a semi-formal approach. Not just regular alarming and metrics.

hipgoat 1y ago

It a comment of assesment

purpleidea 1y ago

It's very interesting (I applaud this) that one of the main goals seems to be to make it more approachable as compared to TLA+, but then they go in write it in C# which I consider to be an incredibly unapproachable community and language. I'm not trying to draw the ire of the Microsoft fan boys, and there are certainly smart people working on that, but it's just not going to happen for most people. Had this been in golang, or maybe java, I'm sure many more hands would be digging in! Having said that, I hope this helps bring correctness and validation more into the mainstream. I've been casually following the project for a while now. My long-term goal is to integrate model validation into https://github.com/purpleidea/mgmt/ https://github.com/purpleidea/mgmt/ so if this is an area of interest to you, please let me know!

sylware 1y ago

Hopefully, they have now a reactive security team, because I do not count the harcking bots/ip scanners they are protecting on their "cloud".

osigurdson 1y ago

It is interesting how the industry ended up with things like TDD when it doesn't work for something as simple as a function that adds two numbers together. While not completely useless in some edge cases, its complete lack of any kind of formal underpinnings should have given us a clue. So many bad / unexamined ideas in the Uncle Bob era. Far closer to a religion than anything else (complete with process "rituals" even).