Dynamically typed languages such as Lua avoid static types in favor of simplicity and exibility, because the absence of static types means that programmers do not need to bother with abstracting types that should be validated by a type checker. In contrast, statically typed languages provide the early detection of many bugs, and a better framework for structuring large programs. These are two advantages of static typing that may lead programmers to migrate from a dynamically typed to a statically typed language, when their simple scripts evolve into complex programs. Optional type systems allow combining dynamic and static typing in the same language, without affecting its original semantics, making easier this code evolution from dynamic to static typing. Designing an optional type system for a dynamically typed language is challenging, as it should feel natural to programmers that are already familiar with this language. In this work we present and formalize the design of Typed Lua, an optional type system for Lua that introduces novel features to statically type check some Lua idioms and features. Even though Lua shares several characteristics with other dynamically typed languages such as JavaScript, Lua also has several unusual features that are not present in the type system of these languages. These features include functions with exible arity, multiple assignment, functions that are overloaded on the number of return values, and the incremental evolution of record and object types. We discuss how Typed Lua handles these features and our design decisions. Finally, we present the evaluation results that we achieved while using Typed Lua to type existing Lua code.