When the implementation is done, the security of it can be evaluated by reading the smart contracts and client code.
Before the implementation is available, one can read informal descriptions about the contract design to evaluate the design. The extent to which this is sufficient is subjective, of course, but personally there is plenty of detail available for me to understand the design to the extent that I don’t expect to be surprised by anything I didn’t think about if/when it goes on mainnet.
False dichotomy. One can have useful discussion about ideas without requiring formal specification.
Also, I certainly didn’t trust Casper just because “Vitalik approved it”. I read the Casper paper, informally verified the proof, read the smart contract linked in the Casper EIP, and informally checked if it corresponded to the paper.
No one in the world knows how Lightning Network works.
The Lightning smart contracts are available at https://github.com/lightningnetwork/lightning-rfc for everyone to read, and they even include very helpful descriptions of what they smart contracts try to do. I’ve read it, and encourage you to if you’re interested in Layer 2 on Bitcoin.
I don’t see how this follows at all. You can figure out an implied threat model by understanding the design.
BTW there is no absolute security of anything security or insecurity of something depends on the security model chosen and threats mitigated.
I agree with this, but this seems to undermine your proposed development model. In practice protocol development (IMHO) occurs by people designing the protocol and the security/threat models together, which makes it hard to design one without taking into consideration the other. There’s still no cross-blockchain-community consensus on very basic choices to be made at the layer one security/threat model (see: selfish mining, fee-stealing attacks in a 0-inflation world, verifier’s dilemma, dPoS, weak subjectivity, post-quantum security, 0-conf (amazingly enough), griefing in Casper-FFG, the staking/slashing metagame in PoS). On layer 2, people will probably disagree on how to evaluate griefing and collective action problems (like in MVP).
I think there are absolutely some suggestions in this post about process that I agree with. I personally would like more precise (not necessarily formal) specifications and proofs, as well as more emphasis on the security/threat model. There also seems to be no consensus around the necessity of formal specification as well as formal verification (the FFG paper was, to some extent, and the contract was slated to undergo it, but most dapps today don’t formally verify stuff before launch, and some write rather imprecise specs). But I think most of this is just personal preference, and as long as we seek clarification, welcome/address good-faith criticism, read code and think for ourselves, run independent audits, and don’t rush for mainnet launches too much, it shouldn’t be necessary to drastically change the development process.