Agile methods are now widely used in software engineering organizations, whereas most formal methods are limited to niches and are perceived as inadequate in the context of agile development.

This paper presents a case study of the innovative practices used at Anaplan, a financial planning and analysis software provider, to integrate formal specification within an agile process.

The results show how Behavior-Driven Specification (BDS), by documenting behavior using executable acceptance criteria (EAC), is used to validate the design and implementation of calculation functions in Anaplan’s sparse calculation engine, while keeping all stakeholders aligned on the requirements. We also show that the interaction between the specifiers and the developers allows catching implementation issues at early stages of the development, while allowing the specification to remain amenable to emerging implementation constraints. The validated requirements have enabled the development of a framework to automatically generate extensive test coverage that is used to verify the implementation. As a result, over 200 bugs were caught in the production code before release, not counting the hundreds of issues that BDS allowed developers to detect earlier in the process.

We show that BDS leads to high levels of confidence in the behavioral correctness of software while being fully aligned with agile practices, and proves to be a significant evolution in the field of software development.