Leslie Lamport gave the closing keynote at SCaLE 22x this year, talking about formal methods and TLA+. He mentioned some previous work Amazon has done in that area.
The structure (ontology, taxonomy) is created with ologs, a formal method from category theory. The behavior (choreography) is created with a semi-formal implementation (XState) of a formal method (Finite State Machines)
The user-facing aspect of the software is designed with Concept Design, a semi-formal method from MIT CSAIL.
Creating software with these methods is refreshing and fun. Maybe one day we can reach Tonsky's "Diagrams are code" vision.
"Diagrams are code" exists as ladder diagrams for PLC, from which Structured Text can be derived, which typically are used by PICs for simple to estimate time behavior in very time-sensitive/critical (real-time) control applications.
Stack + dynamic memory and other system resource modeling would need proper models with especially memory life-time visualization being an open research problem, let alone resource tracking being unsolved (Valgrind offers no flexible API, license restrictions, incomplete and other platforms than Linux are less complete etc).
Reads and writes conditioned on arithmetic have all the issues related to complex arithmetic and I am unaware of (time) models for speculation or instruction re-ordering, let alone applied compiler optimizations.
Fascinating approach with ologs and FSMs I've been working on PAELLADOC (https://github.com/jlcases/paelladoc) which applies MECE principles to documentation structure. Similar philosophy but focused on knowledge representation correctness rather than software behavior.
The results align with your experience - structured conceptual foundations make development more intuitive and documentation more valuable for both humans and AI tools.
> we also sought a language that would allow us to model check (and later prove) key aspects of systems designs while being more approachable to programmers.
I find it a bit surprising that TLA+ with PlusCal can be challenging to learn for your average software engineer, could anyone with experience in P show an example of something that can be difficult to express in TLA+ which is significantly easier in P?
TLA+ requires you to think about problems very differently. It is very much not programming.
It took me a long time (and many false starts) to be able to think in TLA. To quote Lamport, the real challenge of TLA+ is learning to think abstractly.
To that, I think plusCal and the teaching materials around it do a disservice to TLA. The familiar syntax hides the wildly different semantics
A key concern I've consistently had regarding formal verification systems is: how does one confirm the accuracy of the verifier itself?
This issue appears to present an intrinsically unsolvable problem, implying that a formally verified system could still contain bugs due to potential issues in the verification software.
While this perspective doesn't necessarily render formal verification impractical, it does introduce certain caveats that, in my experience, are not frequently addressed in discussions about these systems.
I'd guess the best approach is similar to security - minimal TCB (trusted computing base) that you can verify by hand, and then construct your proof checker on top, and have it verify itself.
Proof and type checkers have a lot of overlap, so you can gain coverage via the language types.
I can't recall exactly, but I think CakeML (https://cakeml.org/jfp14.pdf) had a precursor lisp prover, written in a verified lisp, so would be amenable to this approach.
This is correct. That's why you have core type theories. Very small, easy to understand and implement in a canonocal way. Other languages can be compiled to them.
A deeply considered take: this is theoretically interesting but in practice matters very little.
It’s like worrying about compiler bugs instead of semantic programming errors. If you are getting to the point where you have machine checked proofs, you are already doing great. It’s way more likely that you have a specification bug or modeling error than an error in the solver.
If you are worried about it, many people have solutions that are very compelling. There are LCF style theorem provers like HOL Light with tiny kernels. But for any real world systems, none of this matters, use any automated solvers you like, it will be fine.
This is not just a problem with formal verification systems. It's a problem intrinsic to math, science and reality.
We call these things axioms. The verifier must be assumed to be true.
For all the axioms in mathematics... we don't know if any of those axioms are actually fully true. They seem to be true because we haven't witnessed a case where they aren't true. This is similar to how we verify programs with unit tests. For the verifier it's the same thing, you treat it like an axiom you "verify" it with tests.
I believe there is a distinction between those concepts.
Axioms are true by their own definition. Therefore, discovering an axiom to be false is a concept that is inherently illogical.
Discovering that a formal verification system produced an incorrect output due to a bug in its implementation is a perfectly well-defined concept and doesn't led to any logical contradictions; unless you axiomatically define the output of formal verification systems to be necessarily correct.
I believe this definition don't make sense in the general case considering the number of vectors that can introduce errors into software.
Verifiers can be based on a small proven kernel. That is not really the issue.
The issue is writing the formal specification. Formal verification is in nutshell just proving the equivalence of two different formal constructs: one that is called the spec and one that is called the system (or program). Writing specs is hard.
Perhaps there is no such thing like absolute truth.
In category theory / ologs, a formal method for knowledge representation, the result is always mathematically sound, yet ologs are prefixed with "According to the author's world view ..."
On the other way truth, even if it's not absolute, it's very expensive.
Lately AWS advocates a middle ground, the lightweight formal methods, which are much cheaper than formal methods yet deliver good enough correctness for their business case.
In the same way MIT CSAIL's Daniel Jackson advocates a semi-formal approach to design likely-correct apps (Concept design)
It seems there is a push for better correctness in software, without the aim of perfectionism.
There are many things people try to do here: multiple implementations of the verifier, formally verified implementations of the verifier in other verification tools, by-hand verification, etc.
I find this highly unlikely. My first day at Amazon I encountered an engineer puzzling over a perfect sine wave in a graph. After looking at the scale I made the comment "oh. you're using 5 minute metrics." Their response was "how could you figure that out just by looking at the graph?" When I replied "Queuing theory and control theory," their response was "what's that?"
Since then, Amazon's hiring practices have only gotten worse. Can you invert a tree? Can you respond "tree" or "hash map" when you're asked what is the best data structure for a specific situation? Can you solve a riddle or code an ill-explained l33tcode problem? Are you sure you can parse HTML with regexes? You're Amazon material.
Did you pay attention to the lecture about formal proofs. TLA+ or Coq/Kami? That's great, but it won't help you get a job at Amazon.
The idea that formal proofs are used anywhere but the most obscure corners of AWS is laughable.
Although... it is a nice paper. Props to Amazon for supporting Ph.D.'s doing pure research that will never impact AWS' systems or processes.
They specifically mention "the P team at AWS". The two following things are perfectly able to be simultaneously true:
* The average Amazon engineer is not expected to have awareness of CS fundamentals that go beyond LeetCode-y challenges
* The average Amazon engineer builds using tools which are each developed by a small core team who _are_ expected to know those fundamentals, and who package up those concepts to be usefully usable without full understanding
(I did 10 years on CDO, and my experience matches yours when interacting with my peers, but every time I interacted with the actual Builder Tools teams I was very aware that lived in different worlds)
> The average Amazon engineer is not expected to have awareness of CS fundamentals that go beyond LeetCode-y challenges
I find this a bit unsettling. There are dozens of great CS schools in the US. Even non-elite BSc programs in EU sometimes teach formal methods.
There are also some good introductory books now, e.g. [1]. Perhaps its time to interview more on concepts and less on algorithmic tricks favored by LeetCode?
I doubt current undergrads can't go beyond LeetCode-like challenges.
We recently did a proof of concept with P for our system, and the reception was warm enough that I expect adoption within the year. I wouldn’t exactly call us obscure, at least in the sense used above—greenfield big data system with a bog-standard mix of AWS services.
I will say that time to productivity with P is low, and, in my experience, it emphasizes practical applicability more so than traditional modeling languages like TLA+ (this point is perhaps somewhat unsubstantiated, but the specific tooling we used is still internal). That is to say, it is fairly easy to sell to management, and I can see momentum already starting to pick up internally. No Ph.D. in formal methods required.
And re: the hiring bar, I agree that the bulk of the distribution lies a bit further left than one would hope/imagine, but there is a long tail, and it only takes a handful of engineers to spearhead a project like this. For maintainability, we are betting on the approachable learning curve, but time will tell.
Thanks for the interesting insight.
1. What would you recommend to model multi-thread or multi-process problems on the same system? Is there a good read to give recommendations?
2. Is there a good overview on trade-offs between CSP, Actor model and other methods for this?
3. Are you aware of any process group models?
Cool anecdote but I'm not sure how reasonable it is to expect every person to have expert domain knowledge and recall of every single computer science field just because they got a job to work at Amazon or any other MAANG company.
OK, I will be the useful idiot. I don't fully understand your anecdote. Could you explain what is exactly it that you perceived and that the other engineer failed to see?
Periodic and regular cycles (sine wave) suggests that there is over correction happening in the system, preventing a stable point. More regular measurements or tempered corrections may be called for.
Concrete example: the system sees it's queue utilization as high so it throttles incoming requests, but for too long, the queue looks super healthy on the next check, so the throttle removed but too long until checking again, and now the util is too high again.
> Teams across AWS that build some of its flagship products—from storage (e.g., Amazon S3, EBS), to databases (e.g., Amazon DynamoDB, MemoryDB, Aurora), to compute (e.g., EC2, IoT)—have been using P to reason about the correctness of their system designs.
Later it more specifically mentions these (I probably missed a few):
S3 index, S3 ShardStore, Firecracker VMM, Aurora DB engine commit protocol, The RSA implementation on Graviton2
If you are wondering "why do formal methods at all?" or "how is AWS using P to gain confidence in correctness of their services?", the following re:Invent 2023 talk answers this question, provides an overview of P, and its impact inside AWS: (Re:Invent 2023 Talk) Gain confidence in system correctness & resilience with Formal Methods (Finding Critical Bugs Early!!) - https://www.youtube.com/watch?v=FdXZXnkMDxs
Readit News
https://www.youtube.com/watch?v=tsSDvflzJbc
> Coding isn't Programming - Closing Keynote with Leslie Lamport - SCaLE 22x
https://www.osequi.com/studies/list/list.html
The structure (ontology, taxonomy) is created with ologs, a formal method from category theory. The behavior (choreography) is created with a semi-formal implementation (XState) of a formal method (Finite State Machines)
The user-facing aspect of the software is designed with Concept Design, a semi-formal method from MIT CSAIL.
Creating software with these methods is refreshing and fun. Maybe one day we can reach Tonsky's "Diagrams are code" vision.
https://tonsky.me/blog/diagrams/
Stack + dynamic memory and other system resource modeling would need proper models with especially memory life-time visualization being an open research problem, let alone resource tracking being unsolved (Valgrind offers no flexible API, license restrictions, incomplete and other platforms than Linux are less complete etc).
Reads and writes conditioned on arithmetic have all the issues related to complex arithmetic and I am unaware of (time) models for speculation or instruction re-ordering, let alone applied compiler optimizations.
The results align with your experience - structured conceptual foundations make development more intuitive and documentation more valuable for both humans and AI tools.
I find it a bit surprising that TLA+ with PlusCal can be challenging to learn for your average software engineer, could anyone with experience in P show an example of something that can be difficult to express in TLA+ which is significantly easier in P?
TLA+ requires you to think about problems very differently. It is very much not programming.
It took me a long time (and many false starts) to be able to think in TLA. To quote Lamport, the real challenge of TLA+ is learning to think abstractly.
To that, I think plusCal and the teaching materials around it do a disservice to TLA. The familiar syntax hides the wildly different semantics
This issue appears to present an intrinsically unsolvable problem, implying that a formally verified system could still contain bugs due to potential issues in the verification software.
While this perspective doesn't necessarily render formal verification impractical, it does introduce certain caveats that, in my experience, are not frequently addressed in discussions about these systems.
I can't recall exactly, but I think CakeML (https://cakeml.org/jfp14.pdf) had a precursor lisp prover, written in a verified lisp, so would be amenable to this approach.
EDIT: think it was this one https://www.schemeworkshop.org/2016/verified-lisp-2016-schem...
It’s like worrying about compiler bugs instead of semantic programming errors. If you are getting to the point where you have machine checked proofs, you are already doing great. It’s way more likely that you have a specification bug or modeling error than an error in the solver.
If you are worried about it, many people have solutions that are very compelling. There are LCF style theorem provers like HOL Light with tiny kernels. But for any real world systems, none of this matters, use any automated solvers you like, it will be fine.
We call these things axioms. The verifier must be assumed to be true.
For all the axioms in mathematics... we don't know if any of those axioms are actually fully true. They seem to be true because we haven't witnessed a case where they aren't true. This is similar to how we verify programs with unit tests. For the verifier it's the same thing, you treat it like an axiom you "verify" it with tests.
Axioms are true by their own definition. Therefore, discovering an axiom to be false is a concept that is inherently illogical.
Discovering that a formal verification system produced an incorrect output due to a bug in its implementation is a perfectly well-defined concept and doesn't led to any logical contradictions; unless you axiomatically define the output of formal verification systems to be necessarily correct.
I believe this definition don't make sense in the general case considering the number of vectors that can introduce errors into software.
The issue is writing the formal specification. Formal verification is in nutshell just proving the equivalence of two different formal constructs: one that is called the spec and one that is called the system (or program). Writing specs is hard.
In category theory / ologs, a formal method for knowledge representation, the result is always mathematically sound, yet ologs are prefixed with "According to the author's world view ..."
On the other way truth, even if it's not absolute, it's very expensive.
Lately AWS advocates a middle ground, the lightweight formal methods, which are much cheaper than formal methods yet deliver good enough correctness for their business case.
In the same way MIT CSAIL's Daniel Jackson advocates a semi-formal approach to design likely-correct apps (Concept design)
It seems there is a push for better correctness in software, without the aim of perfectionism.
What are those?
As far as I can tell, people don't deploy verified or high assurance systems without testing or without online monitoring and independent fail safes.
Since then, Amazon's hiring practices have only gotten worse. Can you invert a tree? Can you respond "tree" or "hash map" when you're asked what is the best data structure for a specific situation? Can you solve a riddle or code an ill-explained l33tcode problem? Are you sure you can parse HTML with regexes? You're Amazon material.
Did you pay attention to the lecture about formal proofs. TLA+ or Coq/Kami? That's great, but it won't help you get a job at Amazon.
The idea that formal proofs are used anywhere but the most obscure corners of AWS is laughable.
Although... it is a nice paper. Props to Amazon for supporting Ph.D.'s doing pure research that will never impact AWS' systems or processes.
* The average Amazon engineer is not expected to have awareness of CS fundamentals that go beyond LeetCode-y challenges
* The average Amazon engineer builds using tools which are each developed by a small core team who _are_ expected to know those fundamentals, and who package up those concepts to be usefully usable without full understanding
(I did 10 years on CDO, and my experience matches yours when interacting with my peers, but every time I interacted with the actual Builder Tools teams I was very aware that lived in different worlds)
I find this a bit unsettling. There are dozens of great CS schools in the US. Even non-elite BSc programs in EU sometimes teach formal methods.
There are also some good introductory books now, e.g. [1]. Perhaps its time to interview more on concepts and less on algorithmic tricks favored by LeetCode?
I doubt current undergrads can't go beyond LeetCode-like challenges.
[1] Formal Methods, An Appetizer. https://link.springer.com/book/10.1007/978-3-030-05156-3
I will say that time to productivity with P is low, and, in my experience, it emphasizes practical applicability more so than traditional modeling languages like TLA+ (this point is perhaps somewhat unsubstantiated, but the specific tooling we used is still internal). That is to say, it is fairly easy to sell to management, and I can see momentum already starting to pick up internally. No Ph.D. in formal methods required.
And re: the hiring bar, I agree that the bulk of the distribution lies a bit further left than one would hope/imagine, but there is a long tail, and it only takes a handful of engineers to spearhead a project like this. For maintainability, we are betting on the approachable learning curve, but time will tell.
In your greenfield big data system, what were the state machines? What states could they be in?
Deleted Comment
Concrete example: the system sees it's queue utilization as high so it throttles incoming requests, but for too long, the queue looks super healthy on the next check, so the throttle removed but too long until checking again, and now the util is too high again.
Deleted Comment
It helped me find all kinds of subtle non-intuitive bugs that would have gone unnoticed had I only used hand coded automatic tests.
Highly recommended.
> Teams across AWS that build some of its flagship products—from storage (e.g., Amazon S3, EBS), to databases (e.g., Amazon DynamoDB, MemoryDB, Aurora), to compute (e.g., EC2, IoT)—have been using P to reason about the correctness of their system designs.
Later it more specifically mentions these (I probably missed a few):
S3 index, S3 ShardStore, Firecracker VMM, Aurora DB engine commit protocol, The RSA implementation on Graviton2
(EDIT: formatting)
Github: https://github.com/p-org/P
Deleted Comment