This is a motion proposal for the long-term R&D of the DFINITY Foundation, as part of the follow-up to this post: Motion Proposals on Long Term R&D Plans (Please read this post for context).
- This project is about machine-checked verification of the IC’s properties. Examples include:
- a. Machine-checked verification of NNS on abstract level
- b. Model based testing of NNS canisters via reference implementations
- c. Machine-checked verification the Wasm code of NNS canisters adhere to formally specified properties
- d. Machine-check interface aspects of the IC abstractly (replay protection, authentication)
- e. Create tools to aid building formally verified canisters on the IC for critical applications (e.g., DeFI, auctions, SNS, etc)
- f. Verify execution, message routing, state manager, consensus as close to code level as possible, Develop abstract model of the full replica
- g. Abstractly model sharding and interaction between subnets
- h. Formal and informal linking of models to the actual IC implementation, in particular critical parts of the NNS
- i. Maintain link between models and evolving implementation
Previous motion proposals have revolved around specific features and tended to have clear, finite goals that are delivered and completed. They tended to be measured in days, weeks, or months.
These motion proposals are different and are defining the long-term plan that the foundation will use, e.g., for hiring and organizational build-out. They have the following traits and patterns:
- Their scope is years, not weeks or months as in previous NNS motions
- They have a broad direction but are active areas of R&D so they do not have an obvious line of execution.
- They involve deep research in cryptography, networking, distributed systems, language, virtual machines, operating systems.
- They are meant to match the strengths of where the DFINITY foundation’s expertise is best suited.
- Work on these proposals will not start immediately.
- There will be many follow-up discussions and proposals on each topic when work is underway and smaller milestones and tasks get defined.
An example may be the R&D for “Scalability” where there will be a team investigating and improving the scalability of the IC at various stages. Different bottlenecks will surface and different goals will be met.
We want to double down on the behaviors we think have worked well. These include:
- Publicly identifying owners of subject areas to engage and discuss their thinking with the community
- Providing periodic updates to the community as things evolve, milestones reached, proposals are needed, etc…
- Presenting more and more R&D thinking early and openly.
This has worked well for the last 6 months so we want to repeat this pattern.
Developer forum intro posted
1-pager from the discussion lead posted
NNS Motion proposal submitted
- Ask questions
- Read 1-pager
- Give feedback
- Vote on the motion proposal
Frankly, we do not expect many nitty-gritty details because these are meant to address projects that go on for long time horizons.
The DFINITY foundation’s only goal is to improve the adoption of the IC so we want to sanity-check the projects we see necessary for growing the IC by having you (the ICP community) tell us what you all think of these active R&D threads we have.
In terms of the current roadmap and proposals executed, those are still being worked on and have priority.
An intellectually honest way to look at this long-term R&D project is to see them as the upstream or “primordial soup” from which more baked projects emerge from. With this lens, these proposals are akin to asking, “what kind of specialties or strengths do we want to make sure DFINITY foundation has built up?”
Most (if not all) projects that the DFINITY foundation has executed or is executing are borne from long-running R&D threads. Even when community feedback tells the foundation, “we need X” or “Y does not work”, it is typically the team with the most relevant R&D area that picks up the short-term feature or project.