Most errors in a software development life cycle are introduced in the requirements phase. Rigorous specifications and automatic analysis can address this problem. However, there are almost no tools that are based on formal analysis that can scale up for business systems. Also, there is very little literature that reports on the usefulness and scalability of formal analysis of industrial-scale business specifications. The Requirements Modeling tool, a tool developed at TRDDC, which is a visual, intuitive yet formal notation with analysis support that finds gaps and inconsistencies in functional requirements, is a rare exception. This paper is an experience report on the tool?s usage for capturing functional requirements for a real life insurance project. Four use cases were modeled and analysed formally, one very complex and the others moderately complex. The results are promising. Around 150 queries were raised, pointing to gaps, inconsistencies or ambiguities in the requirements.