This experience report describes a style of applying symbolic model checking developed over the course of four years at Amazon Web Services (AWS). Lessons learned are drawn from proving properties of numerous C-based systems, e.g., custom hypervisors, encryption code, boot loaders, and an IoT operating system. Using our methodology, we find that we can prove the correctness of industrial low-level C-based systems with reasonable effort and predictability. Furthermore, AWS developers are increasingly writing their own formal specifications. All proofs discussed in this paper are publicly available on GitHub. All proofs and specifications described in the paper are available, under the Apache 2.0 license, on the GitHub repository located at https://github.com/awslabs/aws-c-common/ This is the master repository for AWS C Common library, and is in active use by the AWS C Common development team. The description of the contents of this repository are based off commit b0ea9f35df8934f9e03fc3bab3919d55efd69b88, although they are not expected to change significantly in the future.