Wise Contracts is a library for writing high level formal specification of smart contract logic in Athena as well as writing formal proofs about the contract behaviors.
Wise Contracts is highly experimental and work on it is periodic and spurred by inconveniences I might encounter when I'm speccing things out internally at Khalani.
Hypothetically, test and code generation would be possible from these specs. Subsequently verifying the behavior at the EVM level would also be possible given a formal spec of EVM semantics in Athena.