<commit_before>### [AWS] Amazon S3 Strong Consistency

In Dec 2020, Amazon S3 launched [Strong Consistency](https://aws.amazon.com/s3/consistency/) with guaranteed
[strong read-after-write consistency](https://aws.amazon.com/blogs/aws/amazon-s3-update-strong-read-after-write-consistency/).
The S3 team leveraged automated reasoning for ensuring the correctness of S3's Strong
Consistency design. Werner had a detailed blog post about the challenges involved.

!!! quote "Qoute from Werners blog: [Diving Deep on S3 Consistency](https://www.allthingsdistributed.com/2021/04/s3-strong-consistency.html)"
    Common testing techniques like unit testing and integration testing are valuable,
    necessary tools in any production system. But they aren’t enough when you need to build a
    system with such a high bar for correctness. We want a system that’s “provably correct”,
    not just “probably correct.” So, for strong consistency, we utilized a variety of
    techniques for ensuring that what we built is correct, and continues to be correct as the
    system evolves. We employed integration tests, deductive proofs of our proposed cache
    coherence algorithm, model checking to formalize our consistency design and to demonstrate
    its correctness, and we expanded on our model checking to examine actual runnable code.

P was used for creating formal models of all the core distributed protocols involved in
S3's strong consistency and checking that the system model satisfies the desired
correctness guarantees. Details about P and how it is being used by the S3 team can be
found in the [AWS Pi-Week Talk](https://pages.awscloud.com/pi-week-2021.html):
[**Use of Automated Reasoning for S3 Strong Consistency Launch**](https://www.twitch.tv/videos/962963706?t=0h26m57s).

### [AWS] Amazon IoT Devices: OTA Protocol

AWS FreeRTOS is a real-time operating system designed to run on IoT devices to enable them
to interact easily and reliably with AWS services. The Over the Air (OTA) update<commit_msg>Update casestudies.md<commit_after>### [AWS] Amazon S3 Strong Consistency

In Dec 2020, Amazon S3 launched [Strong Consistency](https://aws.amazon.com/s3/consistency/) with guaranteed
[strong read-after-write consistency](https://aws.amazon.com/blogs/aws/amazon-s3-update-strong-read-after-write-consistency/).
The S3 team leveraged automated reasoning for ensuring the correctness of S3's Strong
Consistency design. Werner had a detailed blog post about the challenges involved.

!!! quote "Qoute from Werners blog: [Diving Deep on S3 Consistency](https://www.allthingsdistributed.com/2021/04/s3-strong-consistency.html)"
    Common testing techniques like unit testing and integration testing are valuable,
    necessary tools in any production system. But they aren’t enough when you need to build a
    system with such a high bar for correctness. We want a system that’s “provably correct”,
    not just “probably correct.” So, for strong consistency, we utilized a variety of
    techniques for ensuring that what we built is correct, and continues to be correct as the
    system evolves. We employed integration tests, deductive proofs of our proposed cache
    coherence algorithm, model checking to formalize our consistency design and to demonstrate
    its correctness, and we expanded on our model checking to examine actual runnable code.

P was used for creating formal models of all the core distributed protocols involved in
S3's strong consistency and checking that the system model satisfies the desired
correctness guarantees. Details about P and how it is being used by the S3 team can be
found in the [AWS Pi-Week Talk](https://pages.awscloud.com/pi-week-2021.html):
[**Use of Automated Reasoning for S3 Strong Consistency Launch**](https://www.twitch.tv/videos/962963706?t=0h15m15s).

### [AWS] Amazon IoT Devices: OTA Protocol

AWS FreeRTOS is a real-time operating system designed to run on IoT devices to enable them
to interact easily and reliably with AWS services. The Over the Air (OTA) update
{'fraction_non_alphanumeric': 0.06562654779593859, 'fraction_numerical': 0.019316493313521546, 'mean_word_length': 4.633193863319386, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 10, 'lorem ipsum': 0, 'www.': 4, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6166220', 'n_tokens_mistral': 1115, 'n_tokens_neox': 1026, 'n_words': 516}