AWS Automated Reasoning Internship (Java, Python, Lean)

I spent two summers (2022,2023) working at the Automated Reasoning Group (ARG) at AWS. The ARG group uses decades of research in programming languages and formal methods to deliver mathematical guarantees about code. You can find out more about ARG here.

During my first summer, I built a data pipeline in Python using AWS services such as Lambda, SQS, and DynamoDB to run benchmarking data pipelines on the cloud. This resulted in a 10x speedup over the previous approach and was deployed to production.

In my second summer, building upon previous experience I built infrastructure to ensure SAT solver correctness using the formally verified proof checkers.

I worked closely with AWS scientists to implement state-of-the-art solutions from research while also writing some minor components in the Lean theorem prover.