From the project’s inception until now, btc-verified has been focused on building up, layer by layer, a very minimal model of consensus. Last month’s post talked about how we can discover hidden subtleties in how something works when we try to formalize it. However, even as we formalize things we have to resist the temptation to merely assume that the precise map we have created actually reflects the reality on the ground. This month, however, I decided to take a stab at anchoring this model to the Bitcoin network as it exists in the real world.

It’s tricky to do this type of thing because it forces us to ask the question how do we know the map matches the territory? How close can we get?

For most software that you want to verify it is an option on the table to simply write the software in a verifiable language, compile that down to code that actually runs on silicon and be on your merry way. Alternatively, if the code you’re trying to verify is pure C code, there are ways to verify the C code directly since C’s operational semantics are small enough to reason somewhat efficiently about.

...read more at proofofkeags.com