4 ms·

And what teams use these methods exactly?

• riknos314 2y ago
  The article directly mentions several. > 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)
  • yarapavan 2y ago
    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 https://www.youtube.com/watch?v=FdXZXnkMDxs Github: https://github.com/p-org/P https://github.com/p-org/P
• jmccarthy 2y ago
  https://aws.amazon.com/verified-permissions/ https://aws.amazon.com/verified-permissions/ (AVP) is a team and product which uses the formally verified Cedar language. https://arxiv.org/abs/2403.04651 https://arxiv.org/abs/2403.04651