Strata: A Unified Foundation for Code Reasoning Tools

ABSTRACT

Automated reasoning tools are achieving success at scale across diverse domains, enabled by a rich ecosystem of analyses (deductive verification, model checking, abstract interpretation, etc.) targeting numerous languages (Java, C, Rust, Python, SystemVerilog, etc.). However, these tools are generally single-purpose, targeting a specific language and/or analysis. This prevents improvements from being reused across toolchains and results in significant duplicated effort. To address this, AWS is developing Strata, a unified framework for code reasoning that enables diverse reasoning applications across multiple front-ends and back-ends through a common foundation.

Strata shares some goals with existing Intermediate Verification Languages (IVLs) such as Boogie, Viper, and Why3, but extends beyond them in three key ways. First, Strata is designed to support many different program analyses, not just the SMT-based deductive verification offered by traditional IVLs. Second, rather than a single intermediate language, Strata provides a family of intermediate languages for expressing programs at different levels of abstraction, along with transformations among them that enable various analyses. Strata also includes general-purpose tools for defining intermediate languages, including a domain-specific framework that automatically generates language definitions, parsers, and (de-)serializers. Third, Strata is implemented in Lean and includes formal semantics and proofs of correctness for its transformations, enabling foundationally sound reasoning across languages and analyses. This is complemented by property-based and differential testing of Strata's implementation.

Strata is open-source and underpins a key pillar of Lean's in-progress CSLib initiative. In this talk, I will give an overview of the Strata platform and discuss opportunities for contributing to Strata and its ecosystem.

BIOGRAPHY

Joshua Cohen is an Applied Scientist in the AWS Automated Reasoning Group. He is broadly interested in formal verification, proof assistants, functional programming, and algorithms. During his PhD studies at Princeton he developed a verified implementation of the Why3 intermediate verification language to improve the soundness guarantees of automated verification tools. Previously he worked on the verification of a real-world Reed-Solomon-based error-correction system for network packets using Rocq and the Verified Software Toolchain (VST).