#[cfg(kani)]
#[kani::proof]
fn verify_success() {
let x: u32 = kani::any();
// estimate_size rejects x >= 4096, so this prevents failure from argument verification panicking
kani::assume(x < 4096);
let y = estimate_size(x);
assert!(y < 10);
}
https://model-checking.github.io/kani/tutorial-first-steps.h...
The "workaround" for PoW is running the PoW computation on hardware that's better suited for the task. Bitcoin mining has been using ASIC for many years now.
Let's say a legitimate user is willing to wait for one minute on a budget phone. Then your PoW is limited to what that phone can compute in one minute. But on the attacker's specialized hardware this computation only costs fractions of a penny, so they are barely hindered by it.
The SHA256 based PoW scheme has a very heavy ASIC advantage. People have tried to design PoW scheme that minimize the custom hardware advantage, but I'm not sure if they managed to close the gap far enough to make PoW feasible for this application.