You know, I'm not really into cryptocurrency, but it does seem like it's contributing to a resurgence of interest in formal methods. So - thank you, cryptocurrency community!
I agree; I've been trying to get employers/coworkers to look into TLA+ or Isabelle (for different things) for years now, and it feels like only after every cryptocurrency started blogging did they start to listen.
I find it funny that the reason we want the cryptocurrencies to be formally verified is because we want rock-solid financial transactions so that this distributed story is always accurate (which is good), but actual banks don't seem to have these same requirements.
NOTE: Could be wrong on that last point, getting my information about banks third-hand, it's possible that banks are using formal verification. Can someone who works at a bank confirm?
This is because banks rely on property rights, which are enforced by courts, whereas cryptocurrencies operate on a "fait accompli" basis (i.e. whoever happens to control the coins, owns them). This means, in the cryptocurrency world, mistakes are irreversible. In conventional finance, this is not usually the case.
Sorry for replying to an old thread, but I wanted to respond to this.
I totally understand why blockchain isn't the standard for everything right now; my statement was in regards to formal methods to ensure correctness. For example, "reversing" a transaction could totally be modeled in TLA+ (and probably other systems, I'm just most familiar with TLA+ than most other systems), which would provide model checking (and possibly even proofs) that you would not otherwise have.
Your English is excellent - as a native speaker I wouldn’t have guessed you had a different mother tongue. ‘Fait accompli’ is used in English with the same meaning. I was trying to make a stupid joke referring to fiat currency… HN is a tough audience, and I’m more of a droll engineer type.
Yeah, which always felt like that would be a great reason to formally verify...If a race condition ends up draining my account of all my money, you can bet that I am going to sue for the lost funds and probably a bunch of other things, which I cannot imagine would be very cheap for the bank. In fact, I would think it would be expensive for them even if it wasn't their fault (e.g. maybe there was no money in my account because I just have bad spending habits and a bad memory).
It seems to me that having every bit of evidence on their end to prove that they are guaranteeing our transactions would be a really good thing....I suppose this solution might just work itself out if banks actually start relying on some kind blockchain to secure their transactions.
That is correct- there are all sorts of human and procedural buffers built into bank operations. Correctness of the system- and there is never just one system, there are at minimum dozens, even in the smallest bank- is not a hard requirement.
In fact you would immediately seek another job if you came from formal methods practice and then saw production code at just about any of the different animals called banks.
>> Is formal verification a required course or curriculum competency for any Computer Science or Software Engineering / Computer Engineering degree programs?
I've worked on safety critical software, but we did not use formal methods. Lots of test and checking for coverage (at asm level). Oodles of static analysis and wading through false positives. Do formal methods usually supplement those or replace some of it? Can provers or formal methodologies scale to safety critical codebases of 100s of ksloc? Whether such codebases should exist, or be better partitioned is a separate issue.
The current crowning achievement of formal methods is, as I understand it, seL4. It is a formally proven microkernel of about 8500 LOC. There's still a while to go until they can scale to 100kLOCs, unfortunately.
A problem with both seL4 and CompCert is that the code written to express the proofs is huge, much larger than code that actually does stuff. This puts a ceiling on the size of the projects we can verify.
F* is a language that tries to address that, by finding proofs with z3, a smt prover; z3 can't prove everything on its own but it cuts down proof code by orders of magnitude. They have written a verified cryptography stack and TLS stack, and want to write a whole verified http stack.
F* (through Low, a verified low-level subset of F) can extract verified code to C, which is kind of the inverse than the seL4 proof: seL4 begins with C code and enriches it with proofs of correctness; hacl* (a verified crypto F* lib) begins with a proven correct F* code and extracts C code (I gather the actual crypto primitives is compiled directly to asm code because C has some problems with constant time stuff). This enables hacl* to make bindings to other languages that can just call C code, like this Rust binding
I've never really worked on anything safety-critical, but I know that at least one real-time operating has been designed and verified with TLA+ [1]. The book is a bit pricey (and used copies don't pop up that often), so I haven't read it, but my understanding is that the developers felt that TLA+ did find bugs.
That said, TLA+ is written separately from the code. There could of course be bugs in the translation of TLA+ -> C...TLA+ is about checking the design itself, not the code.
Not as a monolithic object. You might be able to do it with an almost microkernel approach (whatever you're implementing) with multiple small, well-defined objects with a well-defined protocol between them. That can be very useful. But I doubt you could formally verify their collective behaviour. The space and time complexity of the algorithms is explosive as the number of interacting objects increases.
Yes, they are normally used in conjunction with testing. But they are also used in conjunction with careful systems engineering to minimise the amount of code that needs to go through the most rigerous processes and focus on what really mattered.
I'm curious which static analysis tool you were using. I used to work in SPARK Ada and false positives were not really a thing due to how it worked. But I've heard of others that were much less restrictive which ended up with lots of false positives, or "maybe" cases that then wasted everyone's time. I can see how systems like that would put people right off using them.
Another public good that cryptocurrency has been contributing to is advances in zero knowledge proofs including some really interesting stuff like SNARKs
One thing to highlight how important this may turn out to be:
> Proof-carrying data (PCD) enables a set of parties to carry out an indefinitely long distributed computation where every step along the way is accompanied by a proof of correctness. It generalizes incrementally verifiable computation
This has the potential to remove the element of trust that you currently must place in the provider of computation resources. With SNARKs you can simply ask them to include a proof that they actually performed the computation that is sublinear in the length of the proof and sublinear in the amount of time taken to verify the proof.
Of course this will always be more computationally expensive for the provider of the computation resources to both do the work and provide the proof.
It also seems associated with advances in wider adoption and some progression in state of the art of functional package managers and reproducible builds, which has been nice to see.
To clarify, they implemented the algorithm in Dafny, and then proved that version correct. They did not verify code that will actually run in production.
From the paper:
> Dafny is a practical option for the verification of mission-critical smart contracts, and a possible avenue for adoption could be to extend the Dafny code generator engine to support Solidity … or to automatically translate Solidity into Dafny. We are currently evaluating these options
Additionally it's proving a translation of the algorithm implemented in solidity. Solidity is not what is run on Ethereum, EVM bytecode is. Solidity is compiled down to EVM bytecode and that's what is run.
That seems like another point where a bug could creep in.
I wouldn't be surprised if there was a hard fork to save the deposit contract if there was a critical bug discovered.
I mean if there was a critical bug in the solidity compiler itself that would put the correctness of pretty much every contract into question, right? It seems like a fork would be hard to argue against in that case.
Formal methods are good and all, but you can still run into trouble when you fail to account for everything.
Some years ago, I had to work on a massively distributed system that scaled up or down with minimal communication between nodes, depending on the amount of work the system had. The developer of that scaling algorithm, a mathematician that gives quite a few software talks, and writes books teaching functional programming, wrote a proof for the system, guaranteeing its upper and lower bounds of performance. I was brought in because the system wasn't acting anywhere near those parameters: The worst part was that often it'd not downscale at all. The mathematician pointed at his proof, and therefore at the fact that if there was a problem, it must be a bug somewhere else.
So after learning how to read his proof, executing it, and doing all the typical ops stuff to identify what the system believed was going on at any particular time, it became clear that the proof had a significant flaw: It believed that the amount of work that the system received was perfect information, with no latency. Since the real world has latency, and none of that was accounted for, the proof was guaranteeing success in a universe that is different from ours. Once I modified the model to represent the real information quality, the outcomes were pretty close to what we were seeing in reality, and equally unacceptable.
So proofs are powerful, and maybe there are zero issues in the proof of this smart contract, but formal models and proofs can still fail you, they'll just fail far less often than your typical system made with unit tests and chewing gum.
Chewing gum systems tend not to fail catastrophically though, due to a general lack of trust in the solution. Formal verification often instills a sense of confidence that means few, if any, failsafes are put in place.
The formal method involves using a programming language (a mathematically based, verification oriented language) to verify another module in some other programming language.
I’m sure it strengthens the codebase being verified. But there is a reason systems engineering of involves both verification and validation.
Admittedly I'm being a bit trollish as I say this, but do you get the same feeling from proofs that Pythagorean Theorem is correct?
Proving things correct is much harder than finding counter-examples that they aren't correct. But the methods do work. Their based on sound formal logic. Proofs can have mistakes, certainly, but it's a darn strong signal that their system is correct.
The problem with proving things about software is less in the proof itself and more in the connection between the proof and the real world.
If somebody told me that they had a financial system whose security was based on applying the Pythagorean Theorem to physical triangles, it would raise exactly the same red flags—the theorem itself isn't a question, but it doesn't even try to capture how physical materials might be imperfect or change over time, and those are exactly the sort of inconsistencies a motivated attacker could exploit.
I was going to reply but exactly this - I'll add that the proof work in the article is really interesting and I love to see practical work in formal proofs happening as a result of eth in particular. However 100% proven code on eth I just don't believe is 100% trustworthy.
Another way of phrasing it is that the law of leaky abstractions means that though the code itself might be 100% correct, lower levels can puncture the assumptions and make that correctness moot - IE, unsinkable titanic vibes
And also, as a long time observer of software correctness proof fails, I'm getting the old popcorn popper ready for the first instance where there's a bug and then we'll have explained to us that, well actually, the prover wasn't covering that case...
EXACTLY this. It'll be like - oh we proved it using X, but wrote code using Y and ooops, there is some difference so this doesn't count as a break in the proof. If that's the case, you have not in fact proved the contract, you've proved a different contract or code base.
A lot of folks might think this is you pushawing on ETH because you invested differently, but this is quite literally the established track record. For the uninitiated, this is how we got Ethereum and Ethereum Classic. I'd be interested in some of the downvoters making a sound rebuttal rather than graying you into obsolescence but it's 2021. The filter bubble expands thusly.
Vyper has safe math built in, so you wont get accidental over/underflows. but Solidity also has that now in the newer versions. so its really a preference if you prefer the python-like text.
Fe is also being developed, looks like it has been planned out a bit more than vyper.
But more likely we will see developments of security and proofs in languages like cairo, to be used on zkrollups, where we will also see alternative VMs to the EVM. So there will be lots of options with different tradeoffs between composability/security/efficiency/redundancy.
Huh, I guess my information is out-of-date. It is a fast-moving space. And it’s a shame they’re continuing with Solidity.
I’m wondering how Cardano’s Haskell-based Plutus platform will compare in practice, now that they’re rolling out smart contracts as well. I’m guessing they’re going to have significant adoption issues.
NEAR is WASM based. It's interesting but not nearly as "battle tested" as EVM. ETH2 also can't break any backward compatibility, which makes it easier to just keep going down the EVM route.
I'm not a Ethereum core dev, but this is my understanding:
The EVM is tailor-made to accurately account for the expense of executing programs in a distributed environment. It has a highly heterogeneous addressing scheme. Every opcode has execution cost metering that has been refined over time. Each word is 256 bits to make 256-bit cryptographic operations easier. There's significant tooling around the EVM for writing and analyzing smart contracts. Other EVM-based blockchains would need to migrate in parallel. The skillset of "blockchain application developer" has coalesced around Solidity and the EVM.
Bottom line is that although WASM offers compatibility with non-blockchain tooling, the blockchain-specific needs of Ethereum are so much better served by the EVM that migrating is difficult.
The EVM design choices are tightly bound with the on-chain storage of data. On ethereum you pay for reads (less) and writes (more) but everything is very expensive because it's stored in a merkle tree with computationally expensive operations.
Alot of the WASM experimentation has also included changes around how storage is charged. Specifically NEAR does a deposit system where you have to HODL to store data on chain. That allows them to innovate in the runtime and cost structure and still incentivize blockchain nodes.
So it's not entirely gas accounting for computation, its more pricing for storage that probably keeps eth on EVM indefinitely.
Other experimental chains are must more likely to become robust and trusted and more performant and then eclipse ethereum.
Ethereum considered implementing storage rents, like NEAR, but instead decided to transition to a verkle trie model that permits succinct proofs of state values. State rent presents some serious problems regarding composeability. What the state-of-the-art solution for state rent on resources that are effectively common goods?
They're currently prioritizing moving to proof-of-stake (which will end the need for ethereum mining and its high electricity usage globally) and sharding (which will solve the congestion that's causing very high transaction fees). Using WASM would be nice in some ways but it doesn't solve any high priority problems. Maybe it will happen later once some attention is freed up by these main problems being solved.
Most blockchains require all nodes to process all transactions, limiting the total transaction limit of the system to the rate of the slowest node that's intended to be supported. Ethereum is working on sharding transaction data so that every node only needs to handle all of the transactions of its chosen shard, which will allow the enforced transaction limits to be multiplied by the shard count. There's complexity to this because any single transaction can involve data from multiple shards.
Allowing the global transaction limit to be raised will decrease the competition for blockchain space and massively decrease transaction fees.
There are also other standards being worked on to allow transactions to be made in a way that they don't have to be broadcast to all nodes, which will also allow their transactions to have much cheaper fees. These systems are being developed simultaneously by unaffiliated developers in userspace ("layer 2") rather than by the core Ethereum developers who are working on proof-of-stake and sharding. These systems generally come with their own sets of trade-offs (including what kinds of smart contracts they support and how smoothly they interoperate with outside systems) so they don't completely replace the need for sharding being done by the core developers. ZK rollups and optimistic rollups are some of the main kinds of layer 2 scaling solutions being worked on now.
The problem is with how you define and describe "correctness" - a machine can check that code X matches definition Y, but there can be bugs in the nuances of that formal definition Y, so you effectively just have a different set of code in a different language (that formal definition) that you need to audit.
>a machine can check that code X matches definition Y
You shouldn't just check against a definition Y. Ideally you'd have a set of properties that the contract must hold, then prove that X satisfies those properties. It's generally much easier to specify such properties than to write code implementing them, compare for instance an "is_sorted" function to an efficient "sort" function, so it's not just the same code written in a different language.
> Ideally you'd have a set of properties that the contract must hold, then prove that X satisfies those properties.
The issue is that how do you know you have the correct set of properties that a contract must hold? You might think you have all the properties that you need, but realize later that you missed one that is critical for your desired outcome.
Fair enough, but that problem exists regardless of whether you’ve bothered to formally verify the functionality. Gathering requirements is hard, in other words.
My concern is that the verification will provide a false sense of security. This article, for example, seems to be arguing that the verification means there can’t be flaws. I think misunderstanding requirements is much more likely than they are making it seem.
A "is_facebook" function may not be much easier. Smart contracts like Compound, Uniswap are complex functions; much more complicated than sorting which has an objectively correct answer.
We can do a probabilistic check. Just see how much data is being exfiltrated, if it's greater than a X% we can figure it's either Facebook or the Chinese government. ;-)
I think it is moving there but ecosystem is not there yet. Also it does not help that Ethereum has chosen Solidity which is bastard child of javascript.
Solidity has very very little in common with javascript other than they were both quickly put together languages full of weird spots, and both fairly successful.
Solidity is much closer to being C's mentally challenged grandchild than is to javascript.
I think we will see more work like this, and tools developed to help. but really it comes down to tradeoffs of speed and security, what cant be insured, and the impact of bugs.
you might have an uninsured contract with multiple audits and proofs of correctness, vs an insured contract with one quick review. which one would you put money into?
Yes, but that would invalidate a very large chunk of the possible usecases for eth contracts. After all, if you end up needing the courts anyway you might as well use a normal contract, and the whole advantage of eth contracts - to me at least - appears to be the feature that the eth contract is the entirety of the arrangement. So it can be used between two parties in entirely different jurisdictions without that creating an imbalance.
And when the court orders that the parties do something that the eth contract cannot permit (and has been formally proven to prevent from ever being induced to do), how does the eth contract handle that?
IANAL, but I understood Meeting Of Minds to refer to the need for both parties to a contract to actually agree that a contract exists.
From the wiki page you reference for example:
> The reasoning is that a party should not be held to a contract that they were not even aware existed.
And later on, something directly relevant to this discussion perhaps:
> Mutual assent is vitiated by actions such as fraud, undue influence, duress, mutual mistake, or misrepresentation.
I think that this discussion is more closely related to the legal concept of a Mistake [0], which absolutely can be something that a court might address. Though even that doesn't seem like quite a perfect fit here.
IANAL either but my understanding was that the "meeting of the minds", is not just that a mutual understanding that contract exists but there is an agreement on basis of the contract.
In so far as it relates to Eth, my point was that the meeting of the minds only goes as far as "the code is the contract", and the use case is to eliminate the civil courts combing over intent and who knew what.
You jest, but the halting problem is only unsolvable in the general case. For "most" (but not all) programs it is perfectly possible to prove whether or not they will halt.
The halting problem in Ethereum is "solved" (more like "dealth with") by a very simple technique: every EVM instruction has a cost and you have to provide "gas" to run your smart contract. If you don't provide enough gas, your contract call has zero effect and all the gas you paid is lost.
A contract call that would misbehave is guaranteed to halt: not by itself, but by the EVM, which, when the contract call eventually runs out of gas, shall take care of halting it.
IIRC erlang does reduction based scheduling except with a multiplier related to the number of messages in its mailbox - would be interesting to read a comparison from somebody who understands the runtimes better than I do.
In those cases there are no remedies for bugs. What recourse does a victim have in the case of an exploit? How is such a system supposed to attract users when there are no guarantees that problems will ever resolve in their favor?
Well it's not technically a restriction, though it'd be a lot easier if you wrote contracts in a language that left no room for doubt certainly.
In fact you can't really get away from the need for a clear formal description of what the contract does anyway. If you write it in a more flexible language but only accept it with a proof of some formal properties then those formal properties are in effect the contract.
At which point we reach something I still don't quite understand. If people accept code satisfying those formal properties as 'proven correct', then why aren't the contracts written as those formal properties in the first place?
>then why aren't the contracts written as those formal properties in the first place?
How are you going to enforce the contract? If it's formally verified, the contract is enforced by itself.
Not to mention, I think as a developer accepting a spec that isn't verified is a tough pill to swallow, because any bug no matter the size would mean that you're breaking the contract.
It's a restriction, even if it turns out to be a 95% subset of C, because without restrictions, the halting problem would prevent effective verification.
> In fact you can't really get away from the need for a clear formal description of what the contract does anyway.
The code is its own description. The point is verification: does the code implement the contract?
Without knowing much about the topic, when I hear about code being proven to be correct it makes me think of the Curry-Howard correspondence, which states that proofs and programs are isomorphic to each other. Is this related at all? If programs and proofs are the same thing and you have a proof that a program is correct, is that like having a proof that a proof is correct? In which case it seems like you are getting into the domain of meta-logic.
No, not really. Under Curry-Howard, if you have a total function that returns an integer, you’ve proven that an integer exists. But we knew that already.
To prove non-trivial things, you need more sophisticated types that make interesting assertions about their values, where it’s not immediately obvious how to construct a value of that type. Special proof languages are used for this.
You can’t. The headline is missing a piece of context in that the proved it was free of runtime errors… according to a specification they chose to evaluate it against. What if their specification contained an error? You could verify that specification against another specification, you could even do that formally if you want to. Eventually you have to confront Gödel’s incompleteness theorem, and accept that such a level of proof is not possible.
Formal verification btw is just a formalised methodology for evaluating something against a specification. It doesn’t prove that errors don’t exist, or that the verifier hasn’t managed to independently make their own error. It’s just a rigorous PR.
Eh staking Eth2 fits my risk profile and I dont care if another TheDao incident occurs resulting in loss of my Eth
A state rollback would be extremely disappointing to me, even though that much Eth in the hands of one party would undermine the security of Eth2 (which is why the other state rollback occurred)
This proof is impressive, but doesnt change anything for me whether it is bulletproof or not
You are ok with losing $100k of collateral? I just don't have the fortitude to put that much on the line. I could... but I don't think it is wise.
I still don't believe this migration is going to happen at all. If you look at the PoS blocks from other EVM chains, you see that reorgs happen way too often to be comfortable with $100B of assets.
