But those total systems are, of course, subsets of Ethereum, which means that if you write your program in an obviously finite way, you can use the same inductive proofs you would use for a total language.
Turing completeness makes it hard to prove properties automatically about arbitrary programs, but you can still prove properties about specific programs.
I'm pretty sure that MOST research on program verification has been done in the context of Turing complete systems, from the work of Floyd and Hoare, to the symbolic execution of Deutsch and King, to temporal logic, TLA+, etc.
