Why3 is a platform for deductive program verification. With Why3 you can create industrial strength smart contracts. There is an online tool that you can use to experiment with Why3.
With Why3 you can build a theory that explains a logical system. (Recall this explanation of a logical system in simple terms.)
Why3 has an API.
Why3 leverages the Alt-Ergo SMT solver. Alt-Ergo is open source and has an online version that you can experiment with. Here is information about SMT.
Why3, Alt-Ergo, and SMT answer a lot of questions that I was trying to get answered using my Special Theory of Machine-based Automated Communication of Semantic Information of Financial Statements document.
#####################################