A computer-implemented method assesses operation of a financial computing system (FCS). An assessment computer system generates code for a model of the FCS that comprises a model specification for the FCS and a model environment for the FCS. The code for the model uses a type-system based logical programming language that supports typed recursive functions. The assessment computer system generates mathematical axioms that describe the operation of the FCS by compiling the code for the model and assesses the operation of the financial computer system by analyzing the mathematical axioms.