You asked for a BC in Ada, but this is SPARK, which we use for formal verification of Ada code, so there is no need to also have it in Ada; besides that you can do much more in SPARK than just BC and even Ada has much more powerful type features than any other language which in very many cases makes memory management or pointer handling unnecessary (e.g. you can declare much more things by value on the stack, even with variable lenght data structures).