No smart contract language has a real source-level debugger. You get transaction tracers. You get console.log. You get Tenderly replays with bytecode-level stepping if you're lucky. But you don't get what every other serious language has had for decades: set a breakpoint on your source line, step through statements, inspect your variables, see what the compiler did.
Ora has one now.
Ora is a smart contract language and compiler for the EVM with two design pillars: comptime over runtime—decide as much as possible at compile time, so runtime is the fallback—and formal verification and the solver in the developer workflow, the way Foundry put serious testing into the Solidity workflow. FV and Z3 aren’t a separate research step; they’re in the loop: specs next to code, SMT reports in the build artifacts, counterexamples when a proof fails. Here’s what that looks like.