Strata offers a unified platform for formalizing language syntax and semantics, and implementing automated reasoning applications.
Documentation for Strata's Dialect Definition Metalanguage (DDM) system.
Documentation for Strata Core language definition.
Why the Laurel intermediate analysis language is the way it is: its design goals and the rationale behind its features. Laurel attempts to provide features that are common to Java, Python, and JavaScript.
How a checked Laurel program is lowered to Strata Core: the translation pipeline, its passes and their ordering, and the differences between Laurel and Core.
A task-oriented guide to writing Laurel specifications (assertions, loop invariants, pre- and postconditions, quantifiers, objects, modifies clauses, and old), together with the language reference: types, expressions and statements, procedures, and the typing rules.
Documentation for Strata Core analysis backends: SMT encoding, verification modes, and other program transformations.
Design philosophy for translations between Strata IRs: where translation logic lives, dependency directions, and the hourglass structure around Core.
API documentation for Strata and StrataTest.