linear logic (resources never created out of nowhere or dropped on the ground).
temporal logic (things will end within a predictable timeframe, so users can make decisions based on worst-case computations using interest rates and their discount rate).
gas computation (so users can price their participation and the contracts can decide on suitable collateral amounts).
game-theoretic liveness (if everyone follows their apparent self-interest, the dapp is never stuck but makes progress until completion — or indefinitely, depending)
game-theoretic safety (even if all other users collude to violate the protocol, the honest user will be no worse off than if they others are honest, modulo fixed predictable gas and time expense as computed above).
As in my lavbda presentation: