These pages are scenario-shaped: pick the one that matches the task in front of you. Each one assumes you've worked through the tutorial and read the concepts.
Writing proof obligations Patterns for spec decomposition, frame conditions, and helper lemmas. Reading audit output What every check inspects, what its failures look like, and how to fix them. Foundry interop When to use forge directly, how the two configs stay non-overlapping, and what tama test does.