Session Description

DISCLAIMER: This description and the above abstract have been partially generated by LLM

Overview

AI coding assistants boost development speed, but without discipline they create fragile codebases. This session presents a production-tested, spec-driven workflow that uses Scala’s type system and tooling ecosystem as a verification infrastructure. The final goal is to produce correct code without accumulating technical debt.

The Six Validation Rings

The workflow is organized around six concentric rings, each catching errors the previous one cannot:

• Ring 0 – The Compiler: Strict flags and refined types (Iron library/Smithy IDLs) encode business constraints at the type level, rejecting invalid inputs before LLM output ever runs.
• Ring 1 – Static Analysis: Scalafix and WartRemover enforce functional programming discipline and architectural boundaries through custom rules, acting as machine-checkable preconditions for all subsequent rings.
• Ring 2 – Property-Based Testing: ScalaCheck verifies behavior correctness. LLMs generate properties better than implementations, so properties are defined first in the specs, then the implementation is generated and verified against them. Counterexamples feed back to the LLM as targeted fixes.
• Ring 3 – Mutation Testing: Stryker4s exposes blind spots LLMs reliably create: tests that pass the happy path but miss edge cases. A mutation score below 80% triggers reinforcement, with surviving mutants fed back as prompts.
• Ring 4 – Formal Verification: Stainless provides mathematical proof of correctness for pure, high-stakes logic (e.g., interest calculations), verifying all possible inputs via SMT conditions.
• Ring 5 – Runtime Telemetry: After deployment, otel4s monitors contract conformance and Daut checks temporal event sequences against state machine properties. Violations automatically feed back into Ring 2, tightening the safety net over time.

A concepts inventory is added in the loop to prevent the LLM from reinventing the wheel. Further, a Type Driven Development methodology is enforced by generating first the types and then the code fulfilling them.

Why It Matters

The perceived trade-off between speed and quality is false. Scala’s tools turn quality into a correctness mechanism: sealed ADTs enable exhaustiveness checks, refined types make constraints enforceable, and pure functions enable formal verification.

What Attendees Will Learn

• How to structure specs using EARS semi-formal language as a single source of truth
• How to configure Scala’s compiler and linting tools as automated guardrails
• How to use property-based testing as a first-class generation target
• How to apply mutation testing and formal verification where they add most value
• How to close the loop between production runtime behavior and static verification using a workflow used daily on a 60K-line Scala codebase