IO: Cardano High Assurance Technical Collaboration

System 2mo ago1post
Participation 1 0
Reactions 0 0
Last activity 2mo ago
System 2mo ago

On-chain governance action (Treasury Withdrawals).

**Proposal as pdf: https://ipnso-com.ipns.dweb.link/?cid=QmQBhjELHaMKhYZjwuskHS9NRyvUdiGv69aK8C1H787c5A**Cardano's strongest differentiator is its focus on security and correctness, but the tools that deliver on that promise have so far been the domain of auditors and formal methods experts. This proposal lowers the barrier: it brings automated formal verification, and the full high-assurance toolkit, within reach of every Cardano developer.Two workstreams deliver this. The first extends Blaster, IO's open-source automated formal verification tool, from single-script verification to full DApp-level verification. Blaster has already been used to prove correctness properties on production DApps including Djed and USDCx, and has received strong feedback from the Cardano developer community. Today, extending those results to an entire DApp requires manually decomposing properties and verifying each scri

  • Proposer return address: stake1uy7ucfwsxtv36lz2drg4nw538xswshmg9pw8h2yzqd4qrzgzhyrsg
  • Deposit: 100,000 ADA
  • Submitted: epoch 626
  • Expires: epoch 633

View in explorer