[vc_row type=”in_container” full_screen_row_position=”middle” column_margin=”default” column_direction=”default” column_direction_tablet=”default” column_direction_phone=”default” scene_position=”center” constrain_group_2=”yes” constrain_group_4=”yes” constrain_group_6=”yes” text_color=”dark” text_align=”left” row_border_radius=”none” row_border_radius_applies=”bg” overflow=”visible” overlay_strength=”0.3″ gradient_direction=”left_to_right” shape_divider_position=”bottom” bg_image_animation=”none” gradient_type=”default” shape_type=””][vc_column column_padding=”no-extra-padding” column_padding_tablet=”inherit” column_padding_phone=”inherit” column_padding_position=”all” column_element_direction_desktop=”default” column_element_spacing=”default” desktop_text_alignment=”default” tablet_text_alignment=”default” phone_text_alignment=”default” background_color_opacity=”1″ background_hover_color_opacity=”1″ column_backdrop_filter=”none” column_shadow=”none” column_border_radius=”none” column_link_target=”_self” column_position=”default” gradient_direction=”left_to_right” overlay_strength=”0.3″ width=”1/1″ tablet_width_inherit=”default” animation_type=”default” bg_image_animation=”none” border_type=”simple” column_border_width=”none” column_border_style=”solid”][vc_column_text]As you may know, we at MuKn want to commoditize the blockchain sector by simplifying the use of the tools necessary to make DApps.
That’s where formal methods come in.
They aren’t exclusive to our beautiful industry, since they have been used in many engineering projects and of course in computer science.
For example, the compcert C compiler has been used in the development of flight control an navigation algorithms in the aviation industry, but also in order to reduce costs in the nuclear industry.
DARPA also used these methods to increase the hack-resistance of their drones, Amazon and Microsoft use them to secure their networks, and closer to our everyday life, modern GPUs and CPUs absolutely require those formal methods in order to make sur information is properly computed.
The idea is simple : formal methods are all the techniques we use to make sure our code doesn’t has unwanted side effects, and that it always does what is expected. The hard part of the job is to automate this process.
Of course, one can easily understand that the blockchain industry requires rigorous ways of ensuring the safety of a network : the decentralized world implies that you can’t sue a legal entity if you loose your money…
If there is not company to give your trust to, you have to give your trust to a process, and that process has to be flawless.
For that reason, we applied for a grant during the 5th edition of Cardano’s Catalyst Fund. In case you had missed it, below is the video of our latest advancements in formal verification of the Glow language.
Thanks to our teammate Marcin, who implemented these methods and is still working at MuKn, we’re happy to say that this is far from over, and that we applied for another grant at Catalyst 7.
So if you want to support the Glow language’s safety, you can definitely vote for us before February 3rd.
Your support will be greatly appreciated and will allow us to drastically reduce the risk of a user losing assets due to a design flaw.
To read more about formal methods:
- https://compcert.org/compcert-C.html
- The Institute of Flight System Dynamics at the Technical University of Munich uses CompCert in the development of flight control and navigation algorithms.
- In November 2017 CompCert was successfully qualified by MTU riedrichshafen according to IEC 60880, category A and IEC 61508-3:2010, SCL 3 for a certification project in the nuclear energy domain. The use of CompCert reduced development time and costs.
- https://www.cl.cam.ac.uk/~jrh13/slides/oregonsummerschool-26jul12/slides.pdf
[/vc_column_text][/vc_column][/vc_row]