Transpiler for Solidity to Z3Py?

I was looking to convert Solidity-based smart contracts to Z3Py expressions automatically. Current, i do it manually. Has anyone come across such a transpiler?

Thanks.

Some arguments in favor of such transpiler (which you might already know):

• Verification: By translating Solidity code to Z3py, it becomes possible to use formal verification techniques, such as model checking and theorem proving, to check for errors and vulnerabilities in the contract.

• Automation: Automatic translation from Solidity to Z3py can help automate and speed up the process of formal verification, allowing developers to more easily verify their contracts at scale.

• Flexibility: Z3py is a python API, which means that developers can use it together with a wide range of other libraries and tools in python, making it easy to integrate with other parts of their development process.

• Ease of use: Z3py provides an easy-to-use API, which makes it relatively simple for developers to get started with formal verification, even if they have little experience in the field.

• Open-source Availability: Z3 theorem prover and its python API, Z3py, are open-source, which means that developers can access the source code and make modifications to suit their needs.

• Better performance: Z3 theorem prover has been optimized to perform well on a wide range of mathematical and logical operations, which make it perform better than traditional testing methods in many cases.

• Proven tool: Z3 theorem prover is a widely used and well-established tool in formal verification and program analysis, so by using a transpiler to convert Solidity code to Z3py, developers can leverage the proven capabilities of this tool for their own smart contract development.

Of course there would also be arguments against it! But has anyone come across such a transpiler?

Thanks.