diff --git a/404.html b/404.html index dbf7b7175..93a9513e1 100644 --- a/404.html +++ b/404.html @@ -11,7 +11,7 @@ - + diff --git a/assets/files/formal-verification-ocaml-formal-land-f7fc4aec9c67b261b754474cee1e19eb.pdf b/assets/files/formal-verification-ocaml-formal-land-f7fc4aec9c67b261b754474cee1e19eb.pdf deleted file mode 100644 index 25315deaa..000000000 Binary files a/assets/files/formal-verification-ocaml-formal-land-f7fc4aec9c67b261b754474cee1e19eb.pdf and /dev/null differ diff --git a/assets/js/935f2afb.404b1bbe.js b/assets/js/935f2afb.404b1bbe.js new file mode 100644 index 000000000..484a72838 --- /dev/null +++ b/assets/js/935f2afb.404b1bbe.js @@ -0,0 +1 @@ +"use strict";(self.webpackChunkformal_land=self.webpackChunkformal_land||[]).push([[8581],{5610:o=>{o.exports=JSON.parse('{"pluginId":"default","version":"current","label":"Next","banner":null,"badge":false,"noIndex":false,"className":"docs-version-current","isLast":true,"docsSidebars":{"sidebar":[{"type":"link","label":"\ud83d\udee1\ufe0f Audit Reports","href":"/docs/audit","docId":"audit","unlisted":false},{"type":"category","label":"\ud83d\udee0\ufe0f Tools","items":[{"type":"link","label":"\u25fc\ufe0f coq-of-noir","href":"/docs/tools/coq-of-noir/introduction","docId":"tools/coq-of-noir/introduction","unlisted":false},{"type":"category","label":"\ud83d\udc2b coq-of-ocaml","items":[{"type":"link","label":"Install","href":"/docs/tools/coq-of-ocaml/install","docId":"tools/coq-of-ocaml/install","unlisted":false},{"type":"link","label":"Run","href":"/docs/tools/coq-of-ocaml/run","docId":"tools/coq-of-ocaml/run","unlisted":false},{"type":"link","label":"Cookbook","href":"/docs/tools/coq-of-ocaml/cookbook","docId":"tools/coq-of-ocaml/cookbook","unlisted":false},{"type":"category","label":"Language support","items":[{"type":"link","label":"OCaml core","href":"/docs/tools/coq-of-ocaml/language/ocaml-core","docId":"tools/coq-of-ocaml/language/ocaml-core","unlisted":false},{"type":"link","label":"Type definitions","href":"/docs/tools/coq-of-ocaml/language/type-definitions","docId":"tools/coq-of-ocaml/language/type-definitions","unlisted":false},{"type":"link","label":"Module system","href":"/docs/tools/coq-of-ocaml/language/module-system","docId":"tools/coq-of-ocaml/language/module-system","unlisted":false},{"type":"link","label":"GADTs","href":"/docs/tools/coq-of-ocaml/language/gadts","docId":"tools/coq-of-ocaml/language/gadts","unlisted":false}],"collapsed":true,"collapsible":true,"href":"/docs/tools/coq-of-ocaml/language/"},{"type":"category","label":"Options","items":[{"type":"link","label":"Attributes","href":"/docs/tools/coq-of-ocaml/options/attributes","docId":"tools/coq-of-ocaml/options/attributes","unlisted":false},{"type":"link","label":"Configuration","href":"/docs/tools/coq-of-ocaml/options/configuration","docId":"tools/coq-of-ocaml/options/configuration","unlisted":false}],"collapsed":true,"collapsible":true,"href":"/docs/tools/coq-of-ocaml/options/"},{"type":"category","label":"More","items":[{"type":"link","label":"Examples","href":"/docs/tools/coq-of-ocaml/more/examples","docId":"tools/coq-of-ocaml/more/examples","unlisted":false},{"type":"link","label":"Faq","href":"/docs/tools/coq-of-ocaml/more/faq","docId":"tools/coq-of-ocaml/more/faq","unlisted":false}],"collapsed":true,"collapsible":true,"href":"/docs/tools/coq-of-ocaml/more/"}],"collapsed":true,"collapsible":true,"href":"/docs/tools/coq-of-ocaml/introduction"},{"type":"link","label":"\ud83e\udd80 coq-of-rust","href":"/docs/tools/coq-of-rust/introduction","docId":"tools/coq-of-rust/introduction","unlisted":false},{"type":"link","label":"\ud83e\ude81 coq-of-solidity","href":"/docs/tools/coq-of-solidity/introduction","docId":"tools/coq-of-solidity/introduction","unlisted":false}],"collapsed":true,"collapsible":true},{"type":"category","label":"\ud83d\udc65 Company","items":[{"type":"link","label":"\ud83e\udd9a About","href":"/docs/company/about","docId":"company/about","unlisted":false},{"type":"link","label":"\ud83c\udfc1 Introduction","href":"/docs/company/intro","docId":"company/intro","unlisted":false},{"type":"link","label":"\ud83d\udce3 Claims","href":"/docs/company/claims","docId":"company/claims","unlisted":false},{"type":"link","label":"\ud83e\uddd1\u200d\ud83d\udcbc Careers","href":"/docs/company/careers","docId":"company/careers","unlisted":false},{"type":"link","label":"\ud83d\udcdc Press","href":"/docs/company/press","docId":"company/press","unlisted":false},{"type":"link","label":"\ud83d\uddfa\ufe0f Maps","href":"/docs/company/maps","docId":"company/maps","unlisted":false}],"collapsed":true,"collapsible":true},{"type":"category","label":"\ud83e\udd13 Learn","items":[{"type":"link","label":"\ud83d\udcda Start","href":"/docs/learn/start","docId":"learn/start","unlisted":false}],"collapsed":true,"collapsible":true}]},"docs":{"audit":{"id":"audit","title":"\ud83d\udee1\ufe0f Audit Reports","description":"Reports","sidebar":"sidebar"},"company/about":{"id":"company/about","title":"\ud83e\udd9a About","description":"We started in 2021. We specialize in formal verification, that is to say the exhaustive testing of programs, with a focus on the blockchain industry. We develop innovative solutions \ud83d\ude80 to verify code that was unverifiable before. Most of our code is eventually open-sourced and relies on the proof assistant Coq \ud83d\udc13.","sidebar":"sidebar"},"company/careers":{"id":"company/careers","title":"\ud83e\uddd1\u200d\ud83d\udcbc Careers","description":"Our team is currently complete. In general, we work from Paris or remotely.","sidebar":"sidebar"},"company/claims":{"id":"company/claims","title":"\ud83d\udce3 Claims","description":"Here are our claims.","sidebar":"sidebar"},"company/intro":{"id":"company/intro","title":"\ud83c\udfc1 Introduction","description":"Here we present our project.","sidebar":"sidebar"},"company/maps":{"id":"company/maps","title":"\ud83d\uddfa\ufe0f Maps","description":"Here we put some information about the Web3 space \ud83c\udf19 that we find useful. They information may or may not be accurate. You can reuse them.","sidebar":"sidebar"},"company/press":{"id":"company/press","title":"\ud83d\udcdc Press","description":"Here are some documents you can read or use.","sidebar":"sidebar"},"learn/start":{"id":"learn/start","title":"\ud83d\udcda Start","description":"In this part of the website, we will learn about applying modern formal verification to build software without bugs \ud83c\udf8a.","sidebar":"sidebar"},"services/ocaml-development":{"id":"services/ocaml-development","title":"\ud83d\udc2b OCaml development","description":"We offer our OCaml (or Reason/ReScript/Melange) development services. We work as contractors and our unique rate is $10,000 per month all inclusive. Our work can be terminated without notice period on your side. Some of our developers have more than 10 years of experience in software development, either in embedded systems or in Web applications (front and back). We strive to follow strict schedule and fulfill all customer requirements."},"services/rust-development":{"id":"services/rust-development","title":"\ud83e\udd80 Rust development","description":"We help you build your products by offering Rust development services. We work as contractors only. Some of our developers have more than 10 years of experience in software development, either in embedded systems or in Web applications (front and back). We strive to follow strict schedule and fulfill customer requirements."},"services/solidity-development":{"id":"services/solidity-development","title":"\ud83c\uddf8 Solidity development","description":"We offer our Solidity development services. We work as contractors and our unique rate is $10,000 per month all inclusive. Our work can be terminated without notice period on your side. Some of our developers have more than 10 years of experience in software development, either in embedded systems or in Web applications (front and back). We strive to follow strict schedule and fulfill all customer requirements."},"services/typescript-development":{"id":"services/typescript-development","title":"\ud83c\udf10 TypeScript development","description":"We offer our TypeScript development services \ud83c\udfd7\ufe0f to help you build your applications. We work as contractors and our work can be terminated without notice period on your side \ud83d\udd25. Some of our developers have more than 10 years of experience in software development \ud83e\uddd3, either in embedded systems or in Web applications (front and back). We strive to follow schedule \u23f2\ufe0f and fulfill requirements."},"tools/coq-of-noir/introduction":{"id":"tools/coq-of-noir/introduction","title":"\u25fc\ufe0f coq-of-noir","description":"coq-of-noir is a formal verification tool for Noir programs. With it you can ensure that Noir programs are totally bug-free and secure, assuming a correct specification!","sidebar":"sidebar"},"tools/coq-of-ocaml/cookbook":{"id":"tools/coq-of-ocaml/cookbook","title":"Cookbook","description":"Here we list typical situations where we need to change the OCaml source code so that the translated code compiles in Coq.","sidebar":"sidebar"},"tools/coq-of-ocaml/install":{"id":"tools/coq-of-ocaml/install","title":"Install","description":"We recommend to install the latest stable version of coq-of-ocaml via opam.","sidebar":"sidebar"},"tools/coq-of-ocaml/introduction":{"id":"tools/coq-of-ocaml/introduction","title":"\ud83d\udc2b coq-of-ocaml","description":"This project was funded by the French Government \ud83c\uddeb\ud83c\uddf7 and the Tezos Foundation.","sidebar":"sidebar"},"tools/coq-of-ocaml/language/gadts":{"id":"tools/coq-of-ocaml/language/gadts","title":"GADTs","description":"We provide some support for the OCaml\'s GADTs, which are an advanced form of algebraic data-types. As Coq does not have a direct equivalent for the GADTs, we introduce some axioms guided by the user annotations.","sidebar":"sidebar"},"tools/coq-of-ocaml/language/index":{"id":"tools/coq-of-ocaml/language/index","title":"Language support","description":"In this section we details which parts of the OCaml language are supported, and how they are translated to Coq.","sidebar":"sidebar"},"tools/coq-of-ocaml/language/module-system":{"id":"tools/coq-of-ocaml/language/module-system","title":"Module system","description":"To handle the module system of OCaml, the compiler coq-of-ocaml generates either plain Coq modules or dependent records. It never generates Coq functors or module types. You can use coq-of-ocaml to translate modules, module types, functors and first-class modules.","sidebar":"sidebar"},"tools/coq-of-ocaml/language/ocaml-core":{"id":"tools/coq-of-ocaml/language/ocaml-core","title":"OCaml core","description":"coq-of-ocaml translates the functional core of OCaml to the corresponding Coq constructs. It adds type annotations for each definition. We present how this translation work.","sidebar":"sidebar"},"tools/coq-of-ocaml/language/type-definitions":{"id":"tools/coq-of-ocaml/language/type-definitions","title":"Type definitions","description":"coq-of-ocaml generates the Coq definitions corresponding to OCaml\'s type definitions.","sidebar":"sidebar"},"tools/coq-of-ocaml/more/examples":{"id":"tools/coq-of-ocaml/more/examples","title":"Examples","description":"The main project handled with coq-of-ocaml is the crypto-currency Tezos. The result is in the project:","sidebar":"sidebar"},"tools/coq-of-ocaml/more/faq":{"id":"tools/coq-of-ocaml/more/faq","title":"Faq","description":"Here we answer to some questions you may have when using coq-of-ocaml.","sidebar":"sidebar"},"tools/coq-of-ocaml/more/index":{"id":"tools/coq-of-ocaml/more/index","title":"More","description":"In this section we give you a few more information to guide you in the use of coq-of-ocaml.","sidebar":"sidebar"},"tools/coq-of-ocaml/options/attributes":{"id":"tools/coq-of-ocaml/options/attributes","title":"Attributes","description":"We present the attributes which we can use with coq-of-ocaml. See the attributes documentation of OCaml for general information about the attributes mechanism. Note that the OCaml attributes do not change the behavior of a program. There are there to help developer tools.","sidebar":"sidebar"},"tools/coq-of-ocaml/options/configuration":{"id":"tools/coq-of-ocaml/options/configuration","title":"Configuration","description":"We present the configuration mechanism of coq-of-ocaml to define some global settings. We write the configuration in a file in the JSON format. To run coq-of-ocaml with a configuration file, use the -config option:","sidebar":"sidebar"},"tools/coq-of-ocaml/options/index":{"id":"tools/coq-of-ocaml/options/index","title":"Options","description":"There are two main ways to customize the translation made by coq-of-ocaml:","sidebar":"sidebar"},"tools/coq-of-ocaml/run":{"id":"tools/coq-of-ocaml/run","title":"Run","description":"coq-of-ocaml translates the OCaml files one by one. It uses Merlin to get the typing environment of each file. Thus you should first have a project which works with Merlin. This is generally the case for a project compiled with dune.","sidebar":"sidebar"},"tools/coq-of-rust/introduction":{"id":"tools/coq-of-rust/introduction","title":"\ud83e\udd80 coq-of-rust","description":"This project was funded by the Aleph Zero Foundation.","sidebar":"sidebar"},"tools/coq-of-solidity/introduction":{"id":"tools/coq-of-solidity/introduction","title":"\ud83e\ude81 coq-of-solidity","description":"This project was funded by the Aleph Zero Foundation.","sidebar":"sidebar"},"verification/ocaml":{"id":"verification/ocaml","title":"\ud83d\udc2b OCaml verification","description":"To formally verify OCaml programs we are developing the translator coq-of-ocaml. It translates OCaml code to similar-looking code in the interactive proof assistant Coq. We are then expert in the Coq system and can formally verify arbitrarily complex properties."},"verification/rust":{"id":"verification/rust","title":"\ud83e\udd80 Rust verification","description":"We are working on bringing more formal verification to the Rust community. You can also look at this page that is intending to group all the formal verification efforts on Rust, or at the company Cryspen doing formal verification on Rust."},"verification/solidity":{"id":"verification/solidity","title":"\ud83c\uddf8 Solidity verification","description":"Presentation"},"verification/typescript":{"id":"verification/typescript","title":"\ud83c\udf10 TypeScript verification","description":"\ud83d\udcfd\ufe0f Demo "}}}')}}]); \ No newline at end of file diff --git a/assets/js/935f2afb.62e80fa9.js b/assets/js/935f2afb.62e80fa9.js deleted file mode 100644 index c315817d6..000000000 --- a/assets/js/935f2afb.62e80fa9.js +++ /dev/null @@ -1 +0,0 @@ -"use strict";(self.webpackChunkformal_land=self.webpackChunkformal_land||[]).push([[8581],{5610:o=>{o.exports=JSON.parse('{"pluginId":"default","version":"current","label":"Next","banner":null,"badge":false,"noIndex":false,"className":"docs-version-current","isLast":true,"docsSidebars":{"sidebar":[{"type":"link","label":"\ud83d\udee1\ufe0f Audit Reports","href":"/docs/audit","docId":"audit","unlisted":false},{"type":"category","label":"\ud83d\udee0\ufe0f Tools","items":[{"type":"link","label":"\u25fc\ufe0f coq-of-noir","href":"/docs/tools/coq-of-noir/introduction","docId":"tools/coq-of-noir/introduction","unlisted":false},{"type":"category","label":"\ud83d\udc2b coq-of-ocaml","items":[{"type":"link","label":"Install","href":"/docs/tools/coq-of-ocaml/install","docId":"tools/coq-of-ocaml/install","unlisted":false},{"type":"link","label":"Run","href":"/docs/tools/coq-of-ocaml/run","docId":"tools/coq-of-ocaml/run","unlisted":false},{"type":"link","label":"Cookbook","href":"/docs/tools/coq-of-ocaml/cookbook","docId":"tools/coq-of-ocaml/cookbook","unlisted":false},{"type":"category","label":"Language support","items":[{"type":"link","label":"OCaml core","href":"/docs/tools/coq-of-ocaml/language/ocaml-core","docId":"tools/coq-of-ocaml/language/ocaml-core","unlisted":false},{"type":"link","label":"Type definitions","href":"/docs/tools/coq-of-ocaml/language/type-definitions","docId":"tools/coq-of-ocaml/language/type-definitions","unlisted":false},{"type":"link","label":"Module system","href":"/docs/tools/coq-of-ocaml/language/module-system","docId":"tools/coq-of-ocaml/language/module-system","unlisted":false},{"type":"link","label":"GADTs","href":"/docs/tools/coq-of-ocaml/language/gadts","docId":"tools/coq-of-ocaml/language/gadts","unlisted":false}],"collapsed":true,"collapsible":true,"href":"/docs/tools/coq-of-ocaml/language/"},{"type":"category","label":"Options","items":[{"type":"link","label":"Attributes","href":"/docs/tools/coq-of-ocaml/options/attributes","docId":"tools/coq-of-ocaml/options/attributes","unlisted":false},{"type":"link","label":"Configuration","href":"/docs/tools/coq-of-ocaml/options/configuration","docId":"tools/coq-of-ocaml/options/configuration","unlisted":false}],"collapsed":true,"collapsible":true,"href":"/docs/tools/coq-of-ocaml/options/"},{"type":"category","label":"More","items":[{"type":"link","label":"Examples","href":"/docs/tools/coq-of-ocaml/more/examples","docId":"tools/coq-of-ocaml/more/examples","unlisted":false},{"type":"link","label":"Faq","href":"/docs/tools/coq-of-ocaml/more/faq","docId":"tools/coq-of-ocaml/more/faq","unlisted":false}],"collapsed":true,"collapsible":true,"href":"/docs/tools/coq-of-ocaml/more/"}],"collapsed":true,"collapsible":true,"href":"/docs/tools/coq-of-ocaml/introduction"},{"type":"link","label":"\ud83e\udd80 coq-of-rust","href":"/docs/tools/coq-of-rust/introduction","docId":"tools/coq-of-rust/introduction","unlisted":false},{"type":"link","label":"\ud83e\ude81 coq-of-solidity","href":"/docs/tools/coq-of-solidity/introduction","docId":"tools/coq-of-solidity/introduction","unlisted":false}],"collapsed":true,"collapsible":true},{"type":"category","label":"\ud83d\udc65 Company","items":[{"type":"link","label":"\ud83e\udd9a About","href":"/docs/company/about","docId":"company/about","unlisted":false},{"type":"link","label":"\ud83c\udfc1 Introduction","href":"/docs/company/intro","docId":"company/intro","unlisted":false},{"type":"link","label":"\ud83d\udce3 Claims","href":"/docs/company/claims","docId":"company/claims","unlisted":false},{"type":"link","label":"\ud83e\uddd1\u200d\ud83d\udcbc Careers","href":"/docs/company/careers","docId":"company/careers","unlisted":false},{"type":"link","label":"\ud83d\udcdc Press","href":"/docs/company/press","docId":"company/press","unlisted":false},{"type":"link","label":"\ud83d\uddfa\ufe0f Maps","href":"/docs/company/maps","docId":"company/maps","unlisted":false}],"collapsed":true,"collapsible":true},{"type":"category","label":"\ud83e\udd13 Learn","items":[{"type":"link","label":"\ud83d\udcda Start","href":"/docs/learn/start","docId":"learn/start","unlisted":false}],"collapsed":true,"collapsible":true}]},"docs":{"audit":{"id":"audit","title":"\ud83d\udee1\ufe0f Audit Reports","description":"Reports","sidebar":"sidebar"},"company/about":{"id":"company/about","title":"\ud83e\udd9a About","description":"We started in 2021. We specialize in formal verification, that is to say the exhaustive testing of programs, with a focus on the blockchain industry. We develop innovative solutions \ud83d\ude80 to verify code that was unverifiable before. Most of our code is eventually open-sourced and relies on the proof assistant Coq \ud83d\udc13.","sidebar":"sidebar"},"company/careers":{"id":"company/careers","title":"\ud83e\uddd1\u200d\ud83d\udcbc Careers","description":"Our team is currently complete.","sidebar":"sidebar"},"company/claims":{"id":"company/claims","title":"\ud83d\udce3 Claims","description":"Here are our claims.","sidebar":"sidebar"},"company/intro":{"id":"company/intro","title":"\ud83c\udfc1 Introduction","description":"Here we present our project.","sidebar":"sidebar"},"company/maps":{"id":"company/maps","title":"\ud83d\uddfa\ufe0f Maps","description":"Here we put some information about the Web3 space \ud83c\udf19 that we find useful. They information may or may not be accurate. You can reuse them.","sidebar":"sidebar"},"company/press":{"id":"company/press","title":"\ud83d\udcdc Press","description":"Here are some documents you can read or use.","sidebar":"sidebar"},"learn/start":{"id":"learn/start","title":"\ud83d\udcda Start","description":"In this part of the website, we will learn about applying modern formal verification to build software without bugs \ud83c\udf8a.","sidebar":"sidebar"},"services/ocaml-development":{"id":"services/ocaml-development","title":"\ud83d\udc2b OCaml development","description":"We offer our OCaml (or Reason/ReScript/Melange) development services. We work as contractors and our unique rate is $10,000 per month all inclusive. Our work can be terminated without notice period on your side. Some of our developers have more than 10 years of experience in software development, either in embedded systems or in Web applications (front and back). We strive to follow strict schedule and fulfill all customer requirements."},"services/rust-development":{"id":"services/rust-development","title":"\ud83e\udd80 Rust development","description":"We help you build your products by offering Rust development services. We work as contractors only. Some of our developers have more than 10 years of experience in software development, either in embedded systems or in Web applications (front and back). We strive to follow strict schedule and fulfill customer requirements."},"services/solidity-development":{"id":"services/solidity-development","title":"\ud83c\uddf8 Solidity development","description":"We offer our Solidity development services. We work as contractors and our unique rate is $10,000 per month all inclusive. Our work can be terminated without notice period on your side. Some of our developers have more than 10 years of experience in software development, either in embedded systems or in Web applications (front and back). We strive to follow strict schedule and fulfill all customer requirements."},"services/typescript-development":{"id":"services/typescript-development","title":"\ud83c\udf10 TypeScript development","description":"We offer our TypeScript development services \ud83c\udfd7\ufe0f to help you build your applications. We work as contractors and our work can be terminated without notice period on your side \ud83d\udd25. Some of our developers have more than 10 years of experience in software development \ud83e\uddd3, either in embedded systems or in Web applications (front and back). We strive to follow schedule \u23f2\ufe0f and fulfill requirements."},"tools/coq-of-noir/introduction":{"id":"tools/coq-of-noir/introduction","title":"\u25fc\ufe0f coq-of-noir","description":"coq-of-noir is a formal verification tool for Noir programs. With it you can ensure that Noir programs are totally bug-free and secure, assuming a correct specification!","sidebar":"sidebar"},"tools/coq-of-ocaml/cookbook":{"id":"tools/coq-of-ocaml/cookbook","title":"Cookbook","description":"Here we list typical situations where we need to change the OCaml source code so that the translated code compiles in Coq.","sidebar":"sidebar"},"tools/coq-of-ocaml/install":{"id":"tools/coq-of-ocaml/install","title":"Install","description":"We recommend to install the latest stable version of coq-of-ocaml via opam.","sidebar":"sidebar"},"tools/coq-of-ocaml/introduction":{"id":"tools/coq-of-ocaml/introduction","title":"\ud83d\udc2b coq-of-ocaml","description":"This project was funded by the French Government \ud83c\uddeb\ud83c\uddf7 and the Tezos Foundation.","sidebar":"sidebar"},"tools/coq-of-ocaml/language/gadts":{"id":"tools/coq-of-ocaml/language/gadts","title":"GADTs","description":"We provide some support for the OCaml\'s GADTs, which are an advanced form of algebraic data-types. As Coq does not have a direct equivalent for the GADTs, we introduce some axioms guided by the user annotations.","sidebar":"sidebar"},"tools/coq-of-ocaml/language/index":{"id":"tools/coq-of-ocaml/language/index","title":"Language support","description":"In this section we details which parts of the OCaml language are supported, and how they are translated to Coq.","sidebar":"sidebar"},"tools/coq-of-ocaml/language/module-system":{"id":"tools/coq-of-ocaml/language/module-system","title":"Module system","description":"To handle the module system of OCaml, the compiler coq-of-ocaml generates either plain Coq modules or dependent records. It never generates Coq functors or module types. You can use coq-of-ocaml to translate modules, module types, functors and first-class modules.","sidebar":"sidebar"},"tools/coq-of-ocaml/language/ocaml-core":{"id":"tools/coq-of-ocaml/language/ocaml-core","title":"OCaml core","description":"coq-of-ocaml translates the functional core of OCaml to the corresponding Coq constructs. It adds type annotations for each definition. We present how this translation work.","sidebar":"sidebar"},"tools/coq-of-ocaml/language/type-definitions":{"id":"tools/coq-of-ocaml/language/type-definitions","title":"Type definitions","description":"coq-of-ocaml generates the Coq definitions corresponding to OCaml\'s type definitions.","sidebar":"sidebar"},"tools/coq-of-ocaml/more/examples":{"id":"tools/coq-of-ocaml/more/examples","title":"Examples","description":"The main project handled with coq-of-ocaml is the crypto-currency Tezos. The result is in the project:","sidebar":"sidebar"},"tools/coq-of-ocaml/more/faq":{"id":"tools/coq-of-ocaml/more/faq","title":"Faq","description":"Here we answer to some questions you may have when using coq-of-ocaml.","sidebar":"sidebar"},"tools/coq-of-ocaml/more/index":{"id":"tools/coq-of-ocaml/more/index","title":"More","description":"In this section we give you a few more information to guide you in the use of coq-of-ocaml.","sidebar":"sidebar"},"tools/coq-of-ocaml/options/attributes":{"id":"tools/coq-of-ocaml/options/attributes","title":"Attributes","description":"We present the attributes which we can use with coq-of-ocaml. See the attributes documentation of OCaml for general information about the attributes mechanism. Note that the OCaml attributes do not change the behavior of a program. There are there to help developer tools.","sidebar":"sidebar"},"tools/coq-of-ocaml/options/configuration":{"id":"tools/coq-of-ocaml/options/configuration","title":"Configuration","description":"We present the configuration mechanism of coq-of-ocaml to define some global settings. We write the configuration in a file in the JSON format. To run coq-of-ocaml with a configuration file, use the -config option:","sidebar":"sidebar"},"tools/coq-of-ocaml/options/index":{"id":"tools/coq-of-ocaml/options/index","title":"Options","description":"There are two main ways to customize the translation made by coq-of-ocaml:","sidebar":"sidebar"},"tools/coq-of-ocaml/run":{"id":"tools/coq-of-ocaml/run","title":"Run","description":"coq-of-ocaml translates the OCaml files one by one. It uses Merlin to get the typing environment of each file. Thus you should first have a project which works with Merlin. This is generally the case for a project compiled with dune.","sidebar":"sidebar"},"tools/coq-of-rust/introduction":{"id":"tools/coq-of-rust/introduction","title":"\ud83e\udd80 coq-of-rust","description":"This project was funded by the Aleph Zero Foundation.","sidebar":"sidebar"},"tools/coq-of-solidity/introduction":{"id":"tools/coq-of-solidity/introduction","title":"\ud83e\ude81 coq-of-solidity","description":"This project was funded by the Aleph Zero Foundation.","sidebar":"sidebar"},"verification/ocaml":{"id":"verification/ocaml","title":"\ud83d\udc2b OCaml verification","description":"To formally verify OCaml programs we are developing the translator coq-of-ocaml. It translates OCaml code to similar-looking code in the interactive proof assistant Coq. We are then expert in the Coq system and can formally verify arbitrarily complex properties."},"verification/rust":{"id":"verification/rust","title":"\ud83e\udd80 Rust verification","description":"We are working on bringing more formal verification to the Rust community. You can also look at this page that is intending to group all the formal verification efforts on Rust, or at the company Cryspen doing formal verification on Rust."},"verification/solidity":{"id":"verification/solidity","title":"\ud83c\uddf8 Solidity verification","description":"Presentation"},"verification/typescript":{"id":"verification/typescript","title":"\ud83c\udf10 TypeScript verification","description":"\ud83d\udcfd\ufe0f Demo "}}}')}}]); \ No newline at end of file diff --git a/assets/js/9cf8b934.76d29dee.js b/assets/js/9cf8b934.76d29dee.js deleted file mode 100644 index 5ffedf5fb..000000000 --- a/assets/js/9cf8b934.76d29dee.js +++ /dev/null @@ -1 +0,0 @@ -"use strict";(self.webpackChunkformal_land=self.webpackChunkformal_land||[]).push([[440],{7185:(e,n,r)=>{r.r(n),r.d(n,{assets:()=>i,contentTitle:()=>s,default:()=>m,frontMatter:()=>a,metadata:()=>c,toc:()=>l});var t=r(4848),o=r(8453);const a={},s="\ud83e\uddd1\u200d\ud83d\udcbc Careers",c={id:"company/careers",title:"\ud83e\uddd1\u200d\ud83d\udcbc Careers",description:"Our team is currently complete.",source:"@site/docs/company/careers.md",sourceDirName:"company",slug:"/company/careers",permalink:"/docs/company/careers",draft:!1,unlisted:!1,tags:[],version:"current",frontMatter:{},sidebar:"sidebar",previous:{title:"\ud83d\udce3 Claims",permalink:"/docs/company/claims"},next:{title:"\ud83d\udcdc Press",permalink:"/docs/company/press"}},i={},l=[];function d(e){const n={a:"a",admonition:"admonition",h1:"h1",li:"li",p:"p",ul:"ul",...(0,o.R)(),...e.components};return(0,t.jsxs)(t.Fragment,{children:[(0,t.jsx)(n.h1,{id:"-careers",children:"\ud83e\uddd1\u200d\ud83d\udcbc Careers"}),"\n",(0,t.jsx)(n.admonition,{type:"info",children:(0,t.jsx)(n.p,{children:"Our team is currently complete."})}),"\n",(0,t.jsxs)(n.p,{children:["If you are knowledgeable in functional programming / theorem provers and want to work with us, ",(0,t.jsx)("a",{href:"mailto:contact@formal.land",children:"contact us"}),". We provide positions in Paris or remote."]}),"\n",(0,t.jsxs)(n.ul,{children:["\n",(0,t.jsx)(n.li,{children:(0,t.jsx)(n.a,{target:"_blank","data-noBrokenLinkCheck":!0,href:r(5524).A+"",children:"Coq proof engineer"})}),"\n"]})]})}function m(e={}){const{wrapper:n}={...(0,o.R)(),...e.components};return n?(0,t.jsx)(n,{...e,children:(0,t.jsx)(d,{...e})}):d(e)}},5524:(e,n,r)=>{r.d(n,{A:()=>t});const t=r.p+"assets/files/formal-verification-ocaml-formal-land-f7fc4aec9c67b261b754474cee1e19eb.pdf"},8453:(e,n,r)=>{r.d(n,{R:()=>s,x:()=>c});var t=r(6540);const o={},a=t.createContext(o);function s(e){const n=t.useContext(a);return t.useMemo((function(){return"function"==typeof e?e(n):{...n,...e}}),[n,e])}function c(e){let n;return n=e.disableParentContext?"function"==typeof e.components?e.components(o):e.components||o:s(e.components),t.createElement(a.Provider,{value:n},e.children)}}}]); \ No newline at end of file diff --git a/assets/js/9cf8b934.b74bd8e9.js b/assets/js/9cf8b934.b74bd8e9.js new file mode 100644 index 000000000..cc43f484b --- /dev/null +++ b/assets/js/9cf8b934.b74bd8e9.js @@ -0,0 +1 @@ +"use strict";(self.webpackChunkformal_land=self.webpackChunkformal_land||[]).push([[440],{7185:(e,n,r)=>{r.r(n),r.d(n,{assets:()=>i,contentTitle:()=>a,default:()=>p,frontMatter:()=>s,metadata:()=>c,toc:()=>m});var t=r(4848),o=r(8453);const s={},a="\ud83e\uddd1\u200d\ud83d\udcbc Careers",c={id:"company/careers",title:"\ud83e\uddd1\u200d\ud83d\udcbc Careers",description:"Our team is currently complete. In general, we work from Paris or remotely.",source:"@site/docs/company/careers.md",sourceDirName:"company",slug:"/company/careers",permalink:"/docs/company/careers",draft:!1,unlisted:!1,tags:[],version:"current",frontMatter:{},sidebar:"sidebar",previous:{title:"\ud83d\udce3 Claims",permalink:"/docs/company/claims"},next:{title:"\ud83d\udcdc Press",permalink:"/docs/company/press"}},i={},m=[];function l(e){const n={admonition:"admonition",h1:"h1",p:"p",...(0,o.R)(),...e.components};return(0,t.jsxs)(t.Fragment,{children:[(0,t.jsx)(n.h1,{id:"-careers",children:"\ud83e\uddd1\u200d\ud83d\udcbc Careers"}),"\n",(0,t.jsx)(n.admonition,{type:"info",children:(0,t.jsx)(n.p,{children:"Our team is currently complete. In general, we work from Paris or remotely."})})]})}function p(e={}){const{wrapper:n}={...(0,o.R)(),...e.components};return n?(0,t.jsx)(n,{...e,children:(0,t.jsx)(l,{...e})}):l(e)}},8453:(e,n,r)=>{r.d(n,{R:()=>a,x:()=>c});var t=r(6540);const o={},s=t.createContext(o);function a(e){const n=t.useContext(s);return t.useMemo((function(){return"function"==typeof e?e(n):{...n,...e}}),[n,e])}function c(e){let n;return n=e.disableParentContext?"function"==typeof e.components?e.components(o):e.components||o:a(e.components),t.createElement(s.Provider,{value:n},e.children)}}}]); \ No newline at end of file diff --git a/assets/js/runtime~main.52634624.js b/assets/js/runtime~main.1d7bfe8e.js similarity index 99% rename from assets/js/runtime~main.52634624.js rename to assets/js/runtime~main.1d7bfe8e.js index b920c88a8..b8cc0ea3d 100644 --- a/assets/js/runtime~main.52634624.js +++ b/assets/js/runtime~main.1d7bfe8e.js @@ -1 +1 @@ -(()=>{"use strict";var e,a,c,b,f,d={},t={};function r(e){var a=t[e];if(void 0!==a)return a.exports;var c=t[e]={exports:{}};return d[e].call(c.exports,c,c.exports,r),c.exports}r.m=d,e=[],r.O=(a,c,b,f)=>{if(!c){var d=1/0;for(i=0;i=f)&&Object.keys(r.O).every((e=>r.O[e](c[o])))?c.splice(o--,1):(t=!1,f0&&e[i-1][2]>f;i--)e[i]=e[i-1];e[i]=[c,b,f]},r.n=e=>{var a=e&&e.__esModule?()=>e.default:()=>e;return r.d(a,{a:a}),a},c=Object.getPrototypeOf?e=>Object.getPrototypeOf(e):e=>e.__proto__,r.t=function(e,b){if(1&b&&(e=this(e)),8&b)return e;if("object"==typeof e&&e){if(4&b&&e.__esModule)return e;if(16&b&&"function"==typeof e.then)return e}var f=Object.create(null);r.r(f);var d={};a=a||[null,c({}),c([]),c(c)];for(var t=2&b&&e;"object"==typeof t&&!~a.indexOf(t);t=c(t))Object.getOwnPropertyNames(t).forEach((a=>d[a]=()=>e[a]));return d.default=()=>e,r.d(f,d),f},r.d=(e,a)=>{for(var c in a)r.o(a,c)&&!r.o(e,c)&&Object.defineProperty(e,c,{enumerable:!0,get:a[c]})},r.f={},r.e=e=>Promise.all(Object.keys(r.f).reduce(((a,c)=>(r.f[c](e,a),a)),[])),r.u=e=>"assets/js/"+({55:"601ef4a9",58:"a431aef6",65:"3926085a",111:"ae3cae59",127:"1993cab4",291:"0e068da8",367:"917ab7c2",440:"9cf8b934",468:"40a5438f",469:"7d9726a8",471:"4ab1c6f7",498:"ba3e77ec",501:"b985990b",567:"b488c124",574:"890e518c",621:"25e70bc2",640:"8ca4d6e2",656:"72c84e71",697:"ab9c6cc7",721:"bb3f9e72",727:"f813a603",801:"6fa80661",818:"f32fe326",827:"566fc268",863:"a487208b",878:"c7369102",909:"3c80015b",910:"eb6aa549",952:"282cd1c8",970:"3229a8e9",992:"be355487",1019:"720a56e4",1023:"b13ba252",1040:"e34d4f16",1061:"582c3eb6",1079:"e93a9b61",1130:"37dfae32",1131:"36f6f17a",1194:"11ce4159",1338:"99451683",1339:"f1787281",1377:"615dbb02",1425:"f7d79ded",1444:"e56edc49",1477:"2df98331",1543:"d73ecefa",1599:"cec855a0",1674:"f99ec706",1688:"89bd0f60",1691:"806c182d",1692:"bf1ed0c4",1703:"79c03ce4",1716:"523d8f7d",1801:"424e7040",1805:"c445085e",1826:"1ef21e38",1864:"d94865d5",1921:"59b56f69",1924:"8bd24425",1975:"0d56dc46",1979:"a173baa0",1991:"b2b675dd",2070:"aac014fc",2094:"861700e4",2109:"bd0ed3e1",2159:"7236e08c",2173:"2519c48f",2176:"b3ad03cc",2206:"940891e7",2257:"f3a15648",2258:"bdf7c199",2274:"054c34c3",2323:"70899ae5",2442:"d38380b3",2445:"74ab7bc8",2446:"d127eec6",2458:"0c4678a6",2470:"b146e155",2499:"7f18eb30",2538:"04e6399c",2620:"649e05e5",2644:"1fb147df",2676:"e704f625",2711:"9e4087bc",2728:"aa1d233f",2792:"8000e7cb",2864:"586a608e",2875:"bc490233",2937:"74366370",2962:"eada5b94",2968:"39093f96",3094:"d8ad77ec",3096:"439d3734",3102:"b2203129",3185:"ed3f27c2",3186:"68b0dfa4",3187:"4688d424",3214:"08b4cf62",3249:"ccc49370",3255:"9398d9b4",3290:"b12698d1",3339:"262b9cbb",3362:"d90ac61a",3431:"44ac4dbb",3437:"d31ecc05",3478:"35bc1c84",3568:"7d628d86",3639:"cf149e64",3715:"04f3873c",3787:"9e4c2aa5",3879:"5dc20450",3909:"8e0f4841",3933:"4bbf9573",3956:"305566bb",4002:"452bbf79",4075:"033e8252",4084:"e141b4eb",4116:"fd759d37",4119:"89515ffd",4222:"48ac1a5d",4230:"9072ab31",4282:"4f24d1ff",4347:"9bab1bd5",4354:"2adc0ba4",4358:"ffcdbdee",4402:"0928b497",4412:"fe5bf14f",4414:"f1f43052",4462:"3c0ee67f",4467:"02e13650",4478:"98e459ed",4497:"4071a8ab",4543:"4c1a3a9e",4557:"28295219",4559:"b6190d2c",4566:"bdd52cb1",4576:"f1c3ede6",4583:"1df93b7f",4617:"ae7616e5",4696:"ab4c6d72",4753:"908d74e3",4774:"f261144a",4809:"c190410d",4813:"6875c492",4827:"cce51cf2",4828:"1680c68e",4845:"a7cac7dd",4900:"bd9520f3",4907:"29813ec3",4935:"762ff625",4936:"4e6ea248",4970:"c9adbec0",4997:"a8f0412d",5104:"c6618825",5129:"6870d8e6",5213:"c9eb5c8c",5275:"22b2e39c",5302:"a24beb83",5315:"8db8ac2d",5341:"4cee49ee",5345:"2d92dfb9",5361:"65cc9109",5391:"7c0fea77",5428:"8db1271b",5439:"4d658fd1",5440:"834fe8c4",5452:"e417fa07",5457:"ff6b4ecf",5461:"beec3e5b",5578:"a8e6f3e5",5712:"eec17282",5739:"69205f08",5743:"c4d14b59",5756:"560c153f",5767:"8eb4e46b",5801:"2836b1c5",5845:"e6b868b1",5877:"530ea6aa",5894:"b2f554cd",5916:"a2c017b9",5927:"ea11de6c",5941:"52cd65da",5996:"45d50612",6079:"1681b0a1",6103:"fc3deafd",6171:"3b73c59b",6204:"2240d8ed",6244:"63152ce2",6260:"1c25c29d",6375:"d0b22415",6385:"42af9969",6390:"278479fb",6487:"f8de77c0",6521:"b346e459",6528:"4926660f",6722:"74ae6181",6739:"fde865fd",6804:"51bceda4",6820:"0fb5280d",6837:"232c92ba",6840:"db6bff56",6895:"f4e61408",6924:"1e7a46a0",6940:"16329161",7054:"59025a76",7065:"3ba35b71",7097:"cf3d20aa",7098:"a7bd4aaa",7145:"7aba737b",7175:"f6f9690d",7199:"f21d102b",7224:"91ac000a",7261:"6fd34e84",7266:"094a728b",7358:"be4406bf",7381:"a926bf88",7422:"44c9a67a",7472:"814f3328",7520:"f6ba3702",7545:"60862750",7580:"97c52b50",7608:"8b760ba7",7630:"e566aea2",7643:"a6aa9e1f",7650:"ad4ab9ff",7802:"c5d15731",7816:"3169fffb",7829:"680bc8cf",7838:"ae69f024",7900:"a5d7f2f4",8e3:"0fc5ff8e",8005:"b422d039",8013:"4a2980b2",8033:"a9f31b53",8059:"026ddec0",8209:"01a85c17",8246:"638be742",8305:"396effda",8382:"d41fa627",8387:"8ee64c0c",8401:"17896441",8411:"c5903cab",8457:"a06ffc17",8468:"b6692631",8530:"2e0973e2",8540:"b44e231f",8543:"54a1f05d",8581:"935f2afb",8630:"24926dff",8655:"e494d26d",8674:"f099533d",8718:"ae41b95b",8755:"047b1aeb",8772:"82eef687",8790:"92999a1c",8806:"76bc59ef",8820:"bc196327",8821:"892f03bb",8824:"4a4ddbec",8827:"90c66bca",8924:"661d2f35",8958:"491dd2b3",9030:"9b60c9cc",9048:"a94703ab",9059:"84c5b4db",9089:"c98d3999",9111:"34d4b30d",9166:"90d4f0a7",9267:"a7023ddc",9317:"0228dac2",9324:"e32cc564",9328:"36cb36bb",9347:"d7c1c49e",9363:"09cb7d6a",9384:"13e421cf",9424:"b1f9f584",9453:"65fdface",9464:"0b0e8aeb",9607:"b6982b7f",9611:"0ab8b207",9615:"38e3802c",9623:"3ed9a774",9647:"5e95c892",9729:"0a509f49",9741:"20f81dd5",9780:"3621c1a8",9797:"bee11635",9835:"5ef0175c",9837:"95638c7c",9873:"07c12bb3",9888:"a8fa71a4",9890:"0b4df4b7",9984:"97b22f94"}[e]||e)+"."+{55:"0566bb39",58:"af43e9b0",65:"52bc7bda",111:"27061dfb",127:"3a9ef318",291:"d5641d1d",367:"6701a2e9",440:"76d29dee",468:"cb3b4242",469:"0149afb9",471:"1f64822e",498:"4311351a",501:"cfab5552",567:"854d6339",574:"a4a0b2bd",621:"63a8f50d",640:"af8dbf98",656:"986970ed",697:"c9d01eeb",721:"3f073000",727:"4b9cd53e",801:"15602f23",818:"d751af84",827:"68b2268e",863:"1bc6d62d",878:"956e30ef",909:"a90a7aec",910:"a8e7640e",952:"9c43247e",970:"8091dd17",992:"4f66f214",1019:"1b167f27",1023:"05a5a112",1040:"b9281c81",1061:"0b2a818b",1079:"4cbd2c0b",1130:"6803d05b",1131:"c3f65053",1135:"5688adaf",1194:"cee5523d",1338:"d5971c44",1339:"adc7efb4",1377:"54a223a2",1425:"d7b146ab",1444:"d4cfc3c4",1477:"d132f837",1543:"c1ba3faf",1599:"2090aac8",1674:"de011b59",1688:"c1af74bd",1691:"307569a2",1692:"d37d0c29",1703:"445e72c6",1716:"d4dff65e",1801:"550f1c7f",1805:"7a1e67a5",1826:"159246fb",1864:"ee525089",1921:"9a395a96",1924:"91e9f4e0",1975:"1b9a8408",1979:"af43b3f6",1991:"a6c096d4",2070:"af98a9d7",2094:"33c113c1",2109:"55f0eabc",2159:"c01f14a4",2173:"689cb8cb",2176:"51ccbfcf",2206:"95957777",2237:"75d0c357",2257:"e1c4d741",2258:"5d9bb219",2274:"94ef6ea1",2323:"60f2dd29",2442:"30d2b1ab",2445:"8e057809",2446:"9fd4f11a",2458:"1bce34fb",2470:"f1e87858",2499:"49c841a6",2538:"62874827",2620:"b9024547",2644:"90914a6b",2676:"913e7e1e",2711:"abea12d8",2728:"d12ffd65",2778:"459d8f64",2792:"4b1657cb",2864:"9e36b9fc",2875:"1fcb03e0",2937:"622c4914",2962:"62ae8c5d",2968:"4f1f8dbf",3094:"ba824bf4",3096:"65cc6bd7",3102:"d975815b",3185:"9f3bbfb3",3186:"3fa6f2d9",3187:"a6ffa19c",3214:"a39a8a85",3249:"c436d061",3255:"c1f5101c",3290:"12f9fc49",3339:"031ac7d5",3362:"3d9802c1",3431:"1fdac38f",3437:"87d3f793",3478:"fdae8527",3568:"82871bec",3639:"3f898b18",3715:"f56fcc6f",3787:"fb5bcc44",3879:"9ee7e094",3909:"56628669",3933:"046d339f",3956:"6a301a34",4002:"532e2413",4075:"bee38e71",4084:"0fe5f8c1",4116:"18817edc",4119:"568fe728",4222:"bba114da",4230:"60861135",4282:"e8084434",4347:"917e1a75",4354:"914b11f2",4358:"0a98e02f",4402:"fa1054b1",4412:"281f9e28",4414:"986a7113",4462:"b2e48da1",4467:"51aaa417",4478:"1ac289d7",4497:"e6c0ffb1",4543:"8bd6688c",4557:"69a51e2e",4559:"a8a10549",4566:"718e8bdd",4576:"83e373ba",4583:"1abdc564",4617:"7e2bba99",4696:"5597b9c4",4753:"7908f09d",4774:"3bb47763",4809:"3a8464b4",4813:"c9388d9f",4827:"cd88487a",4828:"86931fb1",4845:"eff847ea",4900:"00d2c290",4907:"c0a449f0",4935:"eefe61ce",4936:"808789e2",4970:"28925304",4997:"d5710eaa",5104:"6956da23",5129:"9c7f689f",5213:"a33d4f7b",5275:"8456260d",5302:"39c5171b",5315:"75ba66f0",5341:"b4126614",5345:"220d2ef1",5361:"93d0d593",5391:"dc63af7e",5428:"010b1de8",5439:"c4687111",5440:"788459cb",5452:"50caf0f1",5457:"c54ec846",5461:"79da6fc9",5578:"66de05ff",5712:"10aeb859",5739:"56ecc9eb",5743:"2a9344a6",5756:"41ded959",5767:"10f39e22",5801:"d99fa637",5845:"436010fd",5877:"cc097bef",5894:"9c36a88e",5916:"3a8cfe67",5927:"c2fc3c6e",5941:"eabf7ad4",5996:"af60c555",6079:"3a5db64e",6103:"a34db9bb",6171:"7f38da2f",6204:"7c254684",6244:"9c4cecc6",6260:"14f324e8",6375:"0ae76ec3",6385:"6035ca6c",6390:"bb0f3448",6487:"810ec2f9",6521:"0f6c907e",6528:"b7af3ce0",6722:"f27bb2e2",6739:"6a43a6f2",6804:"a85d6ede",6820:"2099001b",6837:"769080ce",6840:"e8c3bf9d",6895:"51d962f2",6924:"7222bda8",6940:"48a27581",7054:"30e28783",7065:"4977536c",7097:"dec12943",7098:"bd449a7d",7145:"d9ebecc2",7175:"aa0a4723",7199:"197997a1",7224:"301fb2b3",7261:"51e0f4f3",7266:"32ff0fa8",7358:"87c7aa6f",7381:"5d511376",7422:"98bbfa0c",7472:"1945f849",7520:"a45cd4cc",7545:"5752fad7",7580:"cf02f41b",7608:"6af50133",7630:"73da8de5",7643:"19e21a39",7650:"5cd78671",7802:"32cee3b5",7816:"d7857f76",7829:"3c4c4e84",7838:"3194a050",7900:"fbc15c8f",8e3:"0bc45078",8005:"830866b6",8013:"973656cb",8033:"9f044d65",8059:"c98dbcf1",8209:"de3cf12b",8246:"4919ddae",8305:"8b1c4f04",8382:"c640f9c7",8387:"72e4c6f2",8401:"d4130c19",8411:"0416d517",8457:"1aa47368",8468:"3bedc53e",8530:"f3dd583a",8540:"b4a2a703",8543:"5780d3dc",8581:"62e80fa9",8630:"ef8131f6",8655:"68a422ef",8674:"88ad5309",8706:"959c499a",8718:"705b088b",8755:"971011ce",8772:"d8580b07",8790:"0bfa6533",8806:"16737830",8820:"f63bbeed",8821:"eb814a1d",8824:"29cb0317",8827:"a894595c",8924:"c9be2397",8958:"69886543",9030:"97d019ec",9048:"bfd106c6",9059:"8e27b63f",9089:"90feed96",9111:"b06aed8a",9166:"ca220213",9267:"8a2f5823",9317:"eb9a1920",9324:"dac5d5b3",9328:"85d65ba9",9347:"4d4ec702",9363:"6550bed7",9384:"6d9fb24e",9424:"5cae9820",9453:"bbf89ec9",9464:"c997cb3d",9607:"06adb013",9611:"d28c208b",9615:"467ddc95",9623:"8386ecba",9647:"25919f8a",9729:"86f183e3",9741:"85809e97",9780:"a3411121",9797:"c8d6cb73",9835:"610603d3",9837:"e259b87d",9873:"40d473f0",9888:"8b907f5b",9890:"96c8132b",9984:"442a9d5f"}[e]+".js",r.miniCssF=e=>{},r.g=function(){if("object"==typeof globalThis)return globalThis;try{return this||new Function("return this")()}catch(e){if("object"==typeof window)return window}}(),r.o=(e,a)=>Object.prototype.hasOwnProperty.call(e,a),b={},f="formal-land:",r.l=(e,a,c,d)=>{if(b[e])b[e].push(a);else{var t,o;if(void 0!==c)for(var n=document.getElementsByTagName("script"),i=0;i{t.onerror=t.onload=null,clearTimeout(s);var f=b[e];if(delete b[e],t.parentNode&&t.parentNode.removeChild(t),f&&f.forEach((e=>e(c))),a)return a(c)},s=setTimeout(u.bind(null,void 0,{type:"timeout",target:t}),12e4);t.onerror=u.bind(null,t.onerror),t.onload=u.bind(null,t.onload),o&&document.head.appendChild(t)}},r.r=e=>{"undefined"!=typeof Symbol&&Symbol.toStringTag&&Object.defineProperty(e,Symbol.toStringTag,{value:"Module"}),Object.defineProperty(e,"__esModule",{value:!0})},r.p="/",r.gca=function(e){return e={16329161:"6940",17896441:"8401",28295219:"4557",60862750:"7545",74366370:"2937",99451683:"1338","601ef4a9":"55",a431aef6:"58","3926085a":"65",ae3cae59:"111","1993cab4":"127","0e068da8":"291","917ab7c2":"367","9cf8b934":"440","40a5438f":"468","7d9726a8":"469","4ab1c6f7":"471",ba3e77ec:"498",b985990b:"501",b488c124:"567","890e518c":"574","25e70bc2":"621","8ca4d6e2":"640","72c84e71":"656",ab9c6cc7:"697",bb3f9e72:"721",f813a603:"727","6fa80661":"801",f32fe326:"818","566fc268":"827",a487208b:"863",c7369102:"878","3c80015b":"909",eb6aa549:"910","282cd1c8":"952","3229a8e9":"970",be355487:"992","720a56e4":"1019",b13ba252:"1023",e34d4f16:"1040","582c3eb6":"1061",e93a9b61:"1079","37dfae32":"1130","36f6f17a":"1131","11ce4159":"1194",f1787281:"1339","615dbb02":"1377",f7d79ded:"1425",e56edc49:"1444","2df98331":"1477",d73ecefa:"1543",cec855a0:"1599",f99ec706:"1674","89bd0f60":"1688","806c182d":"1691",bf1ed0c4:"1692","79c03ce4":"1703","523d8f7d":"1716","424e7040":"1801",c445085e:"1805","1ef21e38":"1826",d94865d5:"1864","59b56f69":"1921","8bd24425":"1924","0d56dc46":"1975",a173baa0:"1979",b2b675dd:"1991",aac014fc:"2070","861700e4":"2094",bd0ed3e1:"2109","7236e08c":"2159","2519c48f":"2173",b3ad03cc:"2176","940891e7":"2206",f3a15648:"2257",bdf7c199:"2258","054c34c3":"2274","70899ae5":"2323",d38380b3:"2442","74ab7bc8":"2445",d127eec6:"2446","0c4678a6":"2458",b146e155:"2470","7f18eb30":"2499","04e6399c":"2538","649e05e5":"2620","1fb147df":"2644",e704f625:"2676","9e4087bc":"2711",aa1d233f:"2728","8000e7cb":"2792","586a608e":"2864",bc490233:"2875",eada5b94:"2962","39093f96":"2968",d8ad77ec:"3094","439d3734":"3096",b2203129:"3102",ed3f27c2:"3185","68b0dfa4":"3186","4688d424":"3187","08b4cf62":"3214",ccc49370:"3249","9398d9b4":"3255",b12698d1:"3290","262b9cbb":"3339",d90ac61a:"3362","44ac4dbb":"3431",d31ecc05:"3437","35bc1c84":"3478","7d628d86":"3568",cf149e64:"3639","04f3873c":"3715","9e4c2aa5":"3787","5dc20450":"3879","8e0f4841":"3909","4bbf9573":"3933","305566bb":"3956","452bbf79":"4002","033e8252":"4075",e141b4eb:"4084",fd759d37:"4116","89515ffd":"4119","48ac1a5d":"4222","9072ab31":"4230","4f24d1ff":"4282","9bab1bd5":"4347","2adc0ba4":"4354",ffcdbdee:"4358","0928b497":"4402",fe5bf14f:"4412",f1f43052:"4414","3c0ee67f":"4462","02e13650":"4467","98e459ed":"4478","4071a8ab":"4497","4c1a3a9e":"4543",b6190d2c:"4559",bdd52cb1:"4566",f1c3ede6:"4576","1df93b7f":"4583",ae7616e5:"4617",ab4c6d72:"4696","908d74e3":"4753",f261144a:"4774",c190410d:"4809","6875c492":"4813",cce51cf2:"4827","1680c68e":"4828",a7cac7dd:"4845",bd9520f3:"4900","29813ec3":"4907","762ff625":"4935","4e6ea248":"4936",c9adbec0:"4970",a8f0412d:"4997",c6618825:"5104","6870d8e6":"5129",c9eb5c8c:"5213","22b2e39c":"5275",a24beb83:"5302","8db8ac2d":"5315","4cee49ee":"5341","2d92dfb9":"5345","65cc9109":"5361","7c0fea77":"5391","8db1271b":"5428","4d658fd1":"5439","834fe8c4":"5440",e417fa07:"5452",ff6b4ecf:"5457",beec3e5b:"5461",a8e6f3e5:"5578",eec17282:"5712","69205f08":"5739",c4d14b59:"5743","560c153f":"5756","8eb4e46b":"5767","2836b1c5":"5801",e6b868b1:"5845","530ea6aa":"5877",b2f554cd:"5894",a2c017b9:"5916",ea11de6c:"5927","52cd65da":"5941","45d50612":"5996","1681b0a1":"6079",fc3deafd:"6103","3b73c59b":"6171","2240d8ed":"6204","63152ce2":"6244","1c25c29d":"6260",d0b22415:"6375","42af9969":"6385","278479fb":"6390",f8de77c0:"6487",b346e459:"6521","4926660f":"6528","74ae6181":"6722",fde865fd:"6739","51bceda4":"6804","0fb5280d":"6820","232c92ba":"6837",db6bff56:"6840",f4e61408:"6895","1e7a46a0":"6924","59025a76":"7054","3ba35b71":"7065",cf3d20aa:"7097",a7bd4aaa:"7098","7aba737b":"7145",f6f9690d:"7175",f21d102b:"7199","91ac000a":"7224","6fd34e84":"7261","094a728b":"7266",be4406bf:"7358",a926bf88:"7381","44c9a67a":"7422","814f3328":"7472",f6ba3702:"7520","97c52b50":"7580","8b760ba7":"7608",e566aea2:"7630",a6aa9e1f:"7643",ad4ab9ff:"7650",c5d15731:"7802","3169fffb":"7816","680bc8cf":"7829",ae69f024:"7838",a5d7f2f4:"7900","0fc5ff8e":"8000",b422d039:"8005","4a2980b2":"8013",a9f31b53:"8033","026ddec0":"8059","01a85c17":"8209","638be742":"8246","396effda":"8305",d41fa627:"8382","8ee64c0c":"8387",c5903cab:"8411",a06ffc17:"8457",b6692631:"8468","2e0973e2":"8530",b44e231f:"8540","54a1f05d":"8543","935f2afb":"8581","24926dff":"8630",e494d26d:"8655",f099533d:"8674",ae41b95b:"8718","047b1aeb":"8755","82eef687":"8772","92999a1c":"8790","76bc59ef":"8806",bc196327:"8820","892f03bb":"8821","4a4ddbec":"8824","90c66bca":"8827","661d2f35":"8924","491dd2b3":"8958","9b60c9cc":"9030",a94703ab:"9048","84c5b4db":"9059",c98d3999:"9089","34d4b30d":"9111","90d4f0a7":"9166",a7023ddc:"9267","0228dac2":"9317",e32cc564:"9324","36cb36bb":"9328",d7c1c49e:"9347","09cb7d6a":"9363","13e421cf":"9384",b1f9f584:"9424","65fdface":"9453","0b0e8aeb":"9464",b6982b7f:"9607","0ab8b207":"9611","38e3802c":"9615","3ed9a774":"9623","5e95c892":"9647","0a509f49":"9729","20f81dd5":"9741","3621c1a8":"9780",bee11635:"9797","5ef0175c":"9835","95638c7c":"9837","07c12bb3":"9873",a8fa71a4:"9888","0b4df4b7":"9890","97b22f94":"9984"}[e]||e,r.p+r.u(e)},(()=>{var e={5354:0,1869:0};r.f.j=(a,c)=>{var b=r.o(e,a)?e[a]:void 0;if(0!==b)if(b)c.push(b[2]);else if(/^(1869|5354)$/.test(a))e[a]=0;else{var f=new Promise(((c,f)=>b=e[a]=[c,f]));c.push(b[2]=f);var d=r.p+r.u(a),t=new Error;r.l(d,(c=>{if(r.o(e,a)&&(0!==(b=e[a])&&(e[a]=void 0),b)){var f=c&&("load"===c.type?"missing":c.type),d=c&&c.target&&c.target.src;t.message="Loading chunk "+a+" failed.\n("+f+": "+d+")",t.name="ChunkLoadError",t.type=f,t.request=d,b[1](t)}}),"chunk-"+a,a)}},r.O.j=a=>0===e[a];var a=(a,c)=>{var b,f,d=c[0],t=c[1],o=c[2],n=0;if(d.some((a=>0!==e[a]))){for(b in t)r.o(t,b)&&(r.m[b]=t[b]);if(o)var i=o(r)}for(a&&a(c);n{"use strict";var e,a,c,b,f,d={},t={};function r(e){var a=t[e];if(void 0!==a)return a.exports;var c=t[e]={exports:{}};return d[e].call(c.exports,c,c.exports,r),c.exports}r.m=d,e=[],r.O=(a,c,b,f)=>{if(!c){var d=1/0;for(i=0;i=f)&&Object.keys(r.O).every((e=>r.O[e](c[o])))?c.splice(o--,1):(t=!1,f0&&e[i-1][2]>f;i--)e[i]=e[i-1];e[i]=[c,b,f]},r.n=e=>{var a=e&&e.__esModule?()=>e.default:()=>e;return r.d(a,{a:a}),a},c=Object.getPrototypeOf?e=>Object.getPrototypeOf(e):e=>e.__proto__,r.t=function(e,b){if(1&b&&(e=this(e)),8&b)return e;if("object"==typeof e&&e){if(4&b&&e.__esModule)return e;if(16&b&&"function"==typeof e.then)return e}var f=Object.create(null);r.r(f);var d={};a=a||[null,c({}),c([]),c(c)];for(var t=2&b&&e;"object"==typeof t&&!~a.indexOf(t);t=c(t))Object.getOwnPropertyNames(t).forEach((a=>d[a]=()=>e[a]));return d.default=()=>e,r.d(f,d),f},r.d=(e,a)=>{for(var c in a)r.o(a,c)&&!r.o(e,c)&&Object.defineProperty(e,c,{enumerable:!0,get:a[c]})},r.f={},r.e=e=>Promise.all(Object.keys(r.f).reduce(((a,c)=>(r.f[c](e,a),a)),[])),r.u=e=>"assets/js/"+({55:"601ef4a9",58:"a431aef6",65:"3926085a",111:"ae3cae59",127:"1993cab4",291:"0e068da8",367:"917ab7c2",440:"9cf8b934",468:"40a5438f",469:"7d9726a8",471:"4ab1c6f7",498:"ba3e77ec",501:"b985990b",567:"b488c124",574:"890e518c",621:"25e70bc2",640:"8ca4d6e2",656:"72c84e71",697:"ab9c6cc7",721:"bb3f9e72",727:"f813a603",801:"6fa80661",818:"f32fe326",827:"566fc268",863:"a487208b",878:"c7369102",909:"3c80015b",910:"eb6aa549",952:"282cd1c8",970:"3229a8e9",992:"be355487",1019:"720a56e4",1023:"b13ba252",1040:"e34d4f16",1061:"582c3eb6",1079:"e93a9b61",1130:"37dfae32",1131:"36f6f17a",1194:"11ce4159",1338:"99451683",1339:"f1787281",1377:"615dbb02",1425:"f7d79ded",1444:"e56edc49",1477:"2df98331",1543:"d73ecefa",1599:"cec855a0",1674:"f99ec706",1688:"89bd0f60",1691:"806c182d",1692:"bf1ed0c4",1703:"79c03ce4",1716:"523d8f7d",1801:"424e7040",1805:"c445085e",1826:"1ef21e38",1864:"d94865d5",1921:"59b56f69",1924:"8bd24425",1975:"0d56dc46",1979:"a173baa0",1991:"b2b675dd",2070:"aac014fc",2094:"861700e4",2109:"bd0ed3e1",2159:"7236e08c",2173:"2519c48f",2176:"b3ad03cc",2206:"940891e7",2257:"f3a15648",2258:"bdf7c199",2274:"054c34c3",2323:"70899ae5",2442:"d38380b3",2445:"74ab7bc8",2446:"d127eec6",2458:"0c4678a6",2470:"b146e155",2499:"7f18eb30",2538:"04e6399c",2620:"649e05e5",2644:"1fb147df",2676:"e704f625",2711:"9e4087bc",2728:"aa1d233f",2792:"8000e7cb",2864:"586a608e",2875:"bc490233",2937:"74366370",2962:"eada5b94",2968:"39093f96",3094:"d8ad77ec",3096:"439d3734",3102:"b2203129",3185:"ed3f27c2",3186:"68b0dfa4",3187:"4688d424",3214:"08b4cf62",3249:"ccc49370",3255:"9398d9b4",3290:"b12698d1",3339:"262b9cbb",3362:"d90ac61a",3431:"44ac4dbb",3437:"d31ecc05",3478:"35bc1c84",3568:"7d628d86",3639:"cf149e64",3715:"04f3873c",3787:"9e4c2aa5",3879:"5dc20450",3909:"8e0f4841",3933:"4bbf9573",3956:"305566bb",4002:"452bbf79",4075:"033e8252",4084:"e141b4eb",4116:"fd759d37",4119:"89515ffd",4222:"48ac1a5d",4230:"9072ab31",4282:"4f24d1ff",4347:"9bab1bd5",4354:"2adc0ba4",4358:"ffcdbdee",4402:"0928b497",4412:"fe5bf14f",4414:"f1f43052",4462:"3c0ee67f",4467:"02e13650",4478:"98e459ed",4497:"4071a8ab",4543:"4c1a3a9e",4557:"28295219",4559:"b6190d2c",4566:"bdd52cb1",4576:"f1c3ede6",4583:"1df93b7f",4617:"ae7616e5",4696:"ab4c6d72",4753:"908d74e3",4774:"f261144a",4809:"c190410d",4813:"6875c492",4827:"cce51cf2",4828:"1680c68e",4845:"a7cac7dd",4900:"bd9520f3",4907:"29813ec3",4935:"762ff625",4936:"4e6ea248",4970:"c9adbec0",4997:"a8f0412d",5104:"c6618825",5129:"6870d8e6",5213:"c9eb5c8c",5275:"22b2e39c",5302:"a24beb83",5315:"8db8ac2d",5341:"4cee49ee",5345:"2d92dfb9",5361:"65cc9109",5391:"7c0fea77",5428:"8db1271b",5439:"4d658fd1",5440:"834fe8c4",5452:"e417fa07",5457:"ff6b4ecf",5461:"beec3e5b",5578:"a8e6f3e5",5712:"eec17282",5739:"69205f08",5743:"c4d14b59",5756:"560c153f",5767:"8eb4e46b",5801:"2836b1c5",5845:"e6b868b1",5877:"530ea6aa",5894:"b2f554cd",5916:"a2c017b9",5927:"ea11de6c",5941:"52cd65da",5996:"45d50612",6079:"1681b0a1",6103:"fc3deafd",6171:"3b73c59b",6204:"2240d8ed",6244:"63152ce2",6260:"1c25c29d",6375:"d0b22415",6385:"42af9969",6390:"278479fb",6487:"f8de77c0",6521:"b346e459",6528:"4926660f",6722:"74ae6181",6739:"fde865fd",6804:"51bceda4",6820:"0fb5280d",6837:"232c92ba",6840:"db6bff56",6895:"f4e61408",6924:"1e7a46a0",6940:"16329161",7054:"59025a76",7065:"3ba35b71",7097:"cf3d20aa",7098:"a7bd4aaa",7145:"7aba737b",7175:"f6f9690d",7199:"f21d102b",7224:"91ac000a",7261:"6fd34e84",7266:"094a728b",7358:"be4406bf",7381:"a926bf88",7422:"44c9a67a",7472:"814f3328",7520:"f6ba3702",7545:"60862750",7580:"97c52b50",7608:"8b760ba7",7630:"e566aea2",7643:"a6aa9e1f",7650:"ad4ab9ff",7802:"c5d15731",7816:"3169fffb",7829:"680bc8cf",7838:"ae69f024",7900:"a5d7f2f4",8e3:"0fc5ff8e",8005:"b422d039",8013:"4a2980b2",8033:"a9f31b53",8059:"026ddec0",8209:"01a85c17",8246:"638be742",8305:"396effda",8382:"d41fa627",8387:"8ee64c0c",8401:"17896441",8411:"c5903cab",8457:"a06ffc17",8468:"b6692631",8530:"2e0973e2",8540:"b44e231f",8543:"54a1f05d",8581:"935f2afb",8630:"24926dff",8655:"e494d26d",8674:"f099533d",8718:"ae41b95b",8755:"047b1aeb",8772:"82eef687",8790:"92999a1c",8806:"76bc59ef",8820:"bc196327",8821:"892f03bb",8824:"4a4ddbec",8827:"90c66bca",8924:"661d2f35",8958:"491dd2b3",9030:"9b60c9cc",9048:"a94703ab",9059:"84c5b4db",9089:"c98d3999",9111:"34d4b30d",9166:"90d4f0a7",9267:"a7023ddc",9317:"0228dac2",9324:"e32cc564",9328:"36cb36bb",9347:"d7c1c49e",9363:"09cb7d6a",9384:"13e421cf",9424:"b1f9f584",9453:"65fdface",9464:"0b0e8aeb",9607:"b6982b7f",9611:"0ab8b207",9615:"38e3802c",9623:"3ed9a774",9647:"5e95c892",9729:"0a509f49",9741:"20f81dd5",9780:"3621c1a8",9797:"bee11635",9835:"5ef0175c",9837:"95638c7c",9873:"07c12bb3",9888:"a8fa71a4",9890:"0b4df4b7",9984:"97b22f94"}[e]||e)+"."+{55:"0566bb39",58:"af43e9b0",65:"52bc7bda",111:"27061dfb",127:"3a9ef318",291:"d5641d1d",367:"6701a2e9",440:"b74bd8e9",468:"cb3b4242",469:"0149afb9",471:"1f64822e",498:"4311351a",501:"cfab5552",567:"854d6339",574:"a4a0b2bd",621:"63a8f50d",640:"af8dbf98",656:"986970ed",697:"c9d01eeb",721:"3f073000",727:"4b9cd53e",801:"15602f23",818:"d751af84",827:"68b2268e",863:"1bc6d62d",878:"956e30ef",909:"a90a7aec",910:"a8e7640e",952:"9c43247e",970:"8091dd17",992:"4f66f214",1019:"1b167f27",1023:"05a5a112",1040:"b9281c81",1061:"0b2a818b",1079:"4cbd2c0b",1130:"6803d05b",1131:"c3f65053",1135:"5688adaf",1194:"cee5523d",1338:"d5971c44",1339:"adc7efb4",1377:"54a223a2",1425:"d7b146ab",1444:"d4cfc3c4",1477:"d132f837",1543:"c1ba3faf",1599:"2090aac8",1674:"de011b59",1688:"c1af74bd",1691:"307569a2",1692:"d37d0c29",1703:"445e72c6",1716:"d4dff65e",1801:"550f1c7f",1805:"7a1e67a5",1826:"159246fb",1864:"ee525089",1921:"9a395a96",1924:"91e9f4e0",1975:"1b9a8408",1979:"af43b3f6",1991:"a6c096d4",2070:"af98a9d7",2094:"33c113c1",2109:"55f0eabc",2159:"c01f14a4",2173:"689cb8cb",2176:"51ccbfcf",2206:"95957777",2237:"75d0c357",2257:"e1c4d741",2258:"5d9bb219",2274:"94ef6ea1",2323:"60f2dd29",2442:"30d2b1ab",2445:"8e057809",2446:"9fd4f11a",2458:"1bce34fb",2470:"f1e87858",2499:"49c841a6",2538:"62874827",2620:"b9024547",2644:"90914a6b",2676:"913e7e1e",2711:"abea12d8",2728:"d12ffd65",2778:"459d8f64",2792:"4b1657cb",2864:"9e36b9fc",2875:"1fcb03e0",2937:"622c4914",2962:"62ae8c5d",2968:"4f1f8dbf",3094:"ba824bf4",3096:"65cc6bd7",3102:"d975815b",3185:"9f3bbfb3",3186:"3fa6f2d9",3187:"a6ffa19c",3214:"a39a8a85",3249:"c436d061",3255:"c1f5101c",3290:"12f9fc49",3339:"031ac7d5",3362:"3d9802c1",3431:"1fdac38f",3437:"87d3f793",3478:"fdae8527",3568:"82871bec",3639:"3f898b18",3715:"f56fcc6f",3787:"fb5bcc44",3879:"9ee7e094",3909:"56628669",3933:"046d339f",3956:"6a301a34",4002:"532e2413",4075:"bee38e71",4084:"0fe5f8c1",4116:"18817edc",4119:"568fe728",4222:"bba114da",4230:"60861135",4282:"e8084434",4347:"917e1a75",4354:"914b11f2",4358:"0a98e02f",4402:"fa1054b1",4412:"281f9e28",4414:"986a7113",4462:"b2e48da1",4467:"51aaa417",4478:"1ac289d7",4497:"e6c0ffb1",4543:"8bd6688c",4557:"69a51e2e",4559:"a8a10549",4566:"718e8bdd",4576:"83e373ba",4583:"1abdc564",4617:"7e2bba99",4696:"5597b9c4",4753:"7908f09d",4774:"3bb47763",4809:"3a8464b4",4813:"c9388d9f",4827:"cd88487a",4828:"86931fb1",4845:"eff847ea",4900:"00d2c290",4907:"c0a449f0",4935:"eefe61ce",4936:"808789e2",4970:"28925304",4997:"d5710eaa",5104:"6956da23",5129:"9c7f689f",5213:"a33d4f7b",5275:"8456260d",5302:"39c5171b",5315:"75ba66f0",5341:"b4126614",5345:"220d2ef1",5361:"93d0d593",5391:"dc63af7e",5428:"010b1de8",5439:"c4687111",5440:"788459cb",5452:"50caf0f1",5457:"c54ec846",5461:"79da6fc9",5578:"66de05ff",5712:"10aeb859",5739:"56ecc9eb",5743:"2a9344a6",5756:"41ded959",5767:"10f39e22",5801:"d99fa637",5845:"436010fd",5877:"cc097bef",5894:"9c36a88e",5916:"3a8cfe67",5927:"c2fc3c6e",5941:"eabf7ad4",5996:"af60c555",6079:"3a5db64e",6103:"a34db9bb",6171:"7f38da2f",6204:"7c254684",6244:"9c4cecc6",6260:"14f324e8",6375:"0ae76ec3",6385:"6035ca6c",6390:"bb0f3448",6487:"810ec2f9",6521:"0f6c907e",6528:"b7af3ce0",6722:"f27bb2e2",6739:"6a43a6f2",6804:"a85d6ede",6820:"2099001b",6837:"769080ce",6840:"e8c3bf9d",6895:"51d962f2",6924:"7222bda8",6940:"48a27581",7054:"30e28783",7065:"4977536c",7097:"dec12943",7098:"bd449a7d",7145:"d9ebecc2",7175:"aa0a4723",7199:"197997a1",7224:"301fb2b3",7261:"51e0f4f3",7266:"32ff0fa8",7358:"87c7aa6f",7381:"5d511376",7422:"98bbfa0c",7472:"1945f849",7520:"a45cd4cc",7545:"5752fad7",7580:"cf02f41b",7608:"6af50133",7630:"73da8de5",7643:"19e21a39",7650:"5cd78671",7802:"32cee3b5",7816:"d7857f76",7829:"3c4c4e84",7838:"3194a050",7900:"fbc15c8f",8e3:"0bc45078",8005:"830866b6",8013:"973656cb",8033:"9f044d65",8059:"c98dbcf1",8209:"de3cf12b",8246:"4919ddae",8305:"8b1c4f04",8382:"c640f9c7",8387:"72e4c6f2",8401:"d4130c19",8411:"0416d517",8457:"1aa47368",8468:"3bedc53e",8530:"f3dd583a",8540:"b4a2a703",8543:"5780d3dc",8581:"404b1bbe",8630:"ef8131f6",8655:"68a422ef",8674:"88ad5309",8706:"959c499a",8718:"705b088b",8755:"971011ce",8772:"d8580b07",8790:"0bfa6533",8806:"16737830",8820:"f63bbeed",8821:"eb814a1d",8824:"29cb0317",8827:"a894595c",8924:"c9be2397",8958:"69886543",9030:"97d019ec",9048:"bfd106c6",9059:"8e27b63f",9089:"90feed96",9111:"b06aed8a",9166:"ca220213",9267:"8a2f5823",9317:"eb9a1920",9324:"dac5d5b3",9328:"85d65ba9",9347:"4d4ec702",9363:"6550bed7",9384:"6d9fb24e",9424:"5cae9820",9453:"bbf89ec9",9464:"c997cb3d",9607:"06adb013",9611:"d28c208b",9615:"467ddc95",9623:"8386ecba",9647:"25919f8a",9729:"86f183e3",9741:"85809e97",9780:"a3411121",9797:"c8d6cb73",9835:"610603d3",9837:"e259b87d",9873:"40d473f0",9888:"8b907f5b",9890:"96c8132b",9984:"442a9d5f"}[e]+".js",r.miniCssF=e=>{},r.g=function(){if("object"==typeof globalThis)return globalThis;try{return this||new Function("return this")()}catch(e){if("object"==typeof window)return window}}(),r.o=(e,a)=>Object.prototype.hasOwnProperty.call(e,a),b={},f="formal-land:",r.l=(e,a,c,d)=>{if(b[e])b[e].push(a);else{var t,o;if(void 0!==c)for(var n=document.getElementsByTagName("script"),i=0;i{t.onerror=t.onload=null,clearTimeout(s);var f=b[e];if(delete b[e],t.parentNode&&t.parentNode.removeChild(t),f&&f.forEach((e=>e(c))),a)return a(c)},s=setTimeout(u.bind(null,void 0,{type:"timeout",target:t}),12e4);t.onerror=u.bind(null,t.onerror),t.onload=u.bind(null,t.onload),o&&document.head.appendChild(t)}},r.r=e=>{"undefined"!=typeof Symbol&&Symbol.toStringTag&&Object.defineProperty(e,Symbol.toStringTag,{value:"Module"}),Object.defineProperty(e,"__esModule",{value:!0})},r.p="/",r.gca=function(e){return e={16329161:"6940",17896441:"8401",28295219:"4557",60862750:"7545",74366370:"2937",99451683:"1338","601ef4a9":"55",a431aef6:"58","3926085a":"65",ae3cae59:"111","1993cab4":"127","0e068da8":"291","917ab7c2":"367","9cf8b934":"440","40a5438f":"468","7d9726a8":"469","4ab1c6f7":"471",ba3e77ec:"498",b985990b:"501",b488c124:"567","890e518c":"574","25e70bc2":"621","8ca4d6e2":"640","72c84e71":"656",ab9c6cc7:"697",bb3f9e72:"721",f813a603:"727","6fa80661":"801",f32fe326:"818","566fc268":"827",a487208b:"863",c7369102:"878","3c80015b":"909",eb6aa549:"910","282cd1c8":"952","3229a8e9":"970",be355487:"992","720a56e4":"1019",b13ba252:"1023",e34d4f16:"1040","582c3eb6":"1061",e93a9b61:"1079","37dfae32":"1130","36f6f17a":"1131","11ce4159":"1194",f1787281:"1339","615dbb02":"1377",f7d79ded:"1425",e56edc49:"1444","2df98331":"1477",d73ecefa:"1543",cec855a0:"1599",f99ec706:"1674","89bd0f60":"1688","806c182d":"1691",bf1ed0c4:"1692","79c03ce4":"1703","523d8f7d":"1716","424e7040":"1801",c445085e:"1805","1ef21e38":"1826",d94865d5:"1864","59b56f69":"1921","8bd24425":"1924","0d56dc46":"1975",a173baa0:"1979",b2b675dd:"1991",aac014fc:"2070","861700e4":"2094",bd0ed3e1:"2109","7236e08c":"2159","2519c48f":"2173",b3ad03cc:"2176","940891e7":"2206",f3a15648:"2257",bdf7c199:"2258","054c34c3":"2274","70899ae5":"2323",d38380b3:"2442","74ab7bc8":"2445",d127eec6:"2446","0c4678a6":"2458",b146e155:"2470","7f18eb30":"2499","04e6399c":"2538","649e05e5":"2620","1fb147df":"2644",e704f625:"2676","9e4087bc":"2711",aa1d233f:"2728","8000e7cb":"2792","586a608e":"2864",bc490233:"2875",eada5b94:"2962","39093f96":"2968",d8ad77ec:"3094","439d3734":"3096",b2203129:"3102",ed3f27c2:"3185","68b0dfa4":"3186","4688d424":"3187","08b4cf62":"3214",ccc49370:"3249","9398d9b4":"3255",b12698d1:"3290","262b9cbb":"3339",d90ac61a:"3362","44ac4dbb":"3431",d31ecc05:"3437","35bc1c84":"3478","7d628d86":"3568",cf149e64:"3639","04f3873c":"3715","9e4c2aa5":"3787","5dc20450":"3879","8e0f4841":"3909","4bbf9573":"3933","305566bb":"3956","452bbf79":"4002","033e8252":"4075",e141b4eb:"4084",fd759d37:"4116","89515ffd":"4119","48ac1a5d":"4222","9072ab31":"4230","4f24d1ff":"4282","9bab1bd5":"4347","2adc0ba4":"4354",ffcdbdee:"4358","0928b497":"4402",fe5bf14f:"4412",f1f43052:"4414","3c0ee67f":"4462","02e13650":"4467","98e459ed":"4478","4071a8ab":"4497","4c1a3a9e":"4543",b6190d2c:"4559",bdd52cb1:"4566",f1c3ede6:"4576","1df93b7f":"4583",ae7616e5:"4617",ab4c6d72:"4696","908d74e3":"4753",f261144a:"4774",c190410d:"4809","6875c492":"4813",cce51cf2:"4827","1680c68e":"4828",a7cac7dd:"4845",bd9520f3:"4900","29813ec3":"4907","762ff625":"4935","4e6ea248":"4936",c9adbec0:"4970",a8f0412d:"4997",c6618825:"5104","6870d8e6":"5129",c9eb5c8c:"5213","22b2e39c":"5275",a24beb83:"5302","8db8ac2d":"5315","4cee49ee":"5341","2d92dfb9":"5345","65cc9109":"5361","7c0fea77":"5391","8db1271b":"5428","4d658fd1":"5439","834fe8c4":"5440",e417fa07:"5452",ff6b4ecf:"5457",beec3e5b:"5461",a8e6f3e5:"5578",eec17282:"5712","69205f08":"5739",c4d14b59:"5743","560c153f":"5756","8eb4e46b":"5767","2836b1c5":"5801",e6b868b1:"5845","530ea6aa":"5877",b2f554cd:"5894",a2c017b9:"5916",ea11de6c:"5927","52cd65da":"5941","45d50612":"5996","1681b0a1":"6079",fc3deafd:"6103","3b73c59b":"6171","2240d8ed":"6204","63152ce2":"6244","1c25c29d":"6260",d0b22415:"6375","42af9969":"6385","278479fb":"6390",f8de77c0:"6487",b346e459:"6521","4926660f":"6528","74ae6181":"6722",fde865fd:"6739","51bceda4":"6804","0fb5280d":"6820","232c92ba":"6837",db6bff56:"6840",f4e61408:"6895","1e7a46a0":"6924","59025a76":"7054","3ba35b71":"7065",cf3d20aa:"7097",a7bd4aaa:"7098","7aba737b":"7145",f6f9690d:"7175",f21d102b:"7199","91ac000a":"7224","6fd34e84":"7261","094a728b":"7266",be4406bf:"7358",a926bf88:"7381","44c9a67a":"7422","814f3328":"7472",f6ba3702:"7520","97c52b50":"7580","8b760ba7":"7608",e566aea2:"7630",a6aa9e1f:"7643",ad4ab9ff:"7650",c5d15731:"7802","3169fffb":"7816","680bc8cf":"7829",ae69f024:"7838",a5d7f2f4:"7900","0fc5ff8e":"8000",b422d039:"8005","4a2980b2":"8013",a9f31b53:"8033","026ddec0":"8059","01a85c17":"8209","638be742":"8246","396effda":"8305",d41fa627:"8382","8ee64c0c":"8387",c5903cab:"8411",a06ffc17:"8457",b6692631:"8468","2e0973e2":"8530",b44e231f:"8540","54a1f05d":"8543","935f2afb":"8581","24926dff":"8630",e494d26d:"8655",f099533d:"8674",ae41b95b:"8718","047b1aeb":"8755","82eef687":"8772","92999a1c":"8790","76bc59ef":"8806",bc196327:"8820","892f03bb":"8821","4a4ddbec":"8824","90c66bca":"8827","661d2f35":"8924","491dd2b3":"8958","9b60c9cc":"9030",a94703ab:"9048","84c5b4db":"9059",c98d3999:"9089","34d4b30d":"9111","90d4f0a7":"9166",a7023ddc:"9267","0228dac2":"9317",e32cc564:"9324","36cb36bb":"9328",d7c1c49e:"9347","09cb7d6a":"9363","13e421cf":"9384",b1f9f584:"9424","65fdface":"9453","0b0e8aeb":"9464",b6982b7f:"9607","0ab8b207":"9611","38e3802c":"9615","3ed9a774":"9623","5e95c892":"9647","0a509f49":"9729","20f81dd5":"9741","3621c1a8":"9780",bee11635:"9797","5ef0175c":"9835","95638c7c":"9837","07c12bb3":"9873",a8fa71a4:"9888","0b4df4b7":"9890","97b22f94":"9984"}[e]||e,r.p+r.u(e)},(()=>{var e={5354:0,1869:0};r.f.j=(a,c)=>{var b=r.o(e,a)?e[a]:void 0;if(0!==b)if(b)c.push(b[2]);else if(/^(1869|5354)$/.test(a))e[a]=0;else{var f=new Promise(((c,f)=>b=e[a]=[c,f]));c.push(b[2]=f);var d=r.p+r.u(a),t=new Error;r.l(d,(c=>{if(r.o(e,a)&&(0!==(b=e[a])&&(e[a]=void 0),b)){var f=c&&("load"===c.type?"missing":c.type),d=c&&c.target&&c.target.src;t.message="Loading chunk "+a+" failed.\n("+f+": "+d+")",t.name="ChunkLoadError",t.type=f,t.request=d,b[1](t)}}),"chunk-"+a,a)}},r.O.j=a=>0===e[a];var a=(a,c)=>{var b,f,d=c[0],t=c[1],o=c[2],n=0;if(d.some((a=>0!==e[a]))){for(b in t)r.o(t,b)&&(r.m[b]=t[b]);if(o)var i=o(r)}for(a&&a(c);n - + diff --git a/blog/2021/10/10/welcome.html b/blog/2021/10/10/welcome.html index 46e8f7448..54486a338 100644 --- a/blog/2021/10/10/welcome.html +++ b/blog/2021/10/10/welcome.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2021/10/27/verification-data-encoding.html b/blog/2021/10/27/verification-data-encoding.html index f65ff7338..99d737e4d 100644 --- a/blog/2021/10/27/verification-data-encoding.html +++ b/blog/2021/10/27/verification-data-encoding.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2021/11/12/new-blog-posts-and-meetup-talk.html b/blog/2021/11/12/new-blog-posts-and-meetup-talk.html index 74ee54bbb..c4e3006c7 100644 --- a/blog/2021/11/12/new-blog-posts-and-meetup-talk.html +++ b/blog/2021/11/12/new-blog-posts-and-meetup-talk.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2022/02/02/make-tezos-a-formally-verified-crypto.html b/blog/2022/02/02/make-tezos-a-formally-verified-crypto.html index 037d00e4c..087ba8e16 100644 --- a/blog/2022/02/02/make-tezos-a-formally-verified-crypto.html +++ b/blog/2022/02/02/make-tezos-a-formally-verified-crypto.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2022/06/15/status update-tezos.html b/blog/2022/06/15/status update-tezos.html index 0c9dac0b5..84239659a 100644 --- a/blog/2022/06/15/status update-tezos.html +++ b/blog/2022/06/15/status update-tezos.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2022/06/23/upgrade-coq-of-ocaml-4.14.html b/blog/2022/06/23/upgrade-coq-of-ocaml-4.14.html index 211e254af..c1616997d 100644 --- a/blog/2022/06/23/upgrade-coq-of-ocaml-4.14.html +++ b/blog/2022/06/23/upgrade-coq-of-ocaml-4.14.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2022/12/13/latest-blog-posts-on-tezos.html b/blog/2022/12/13/latest-blog-posts-on-tezos.html index f3bb19a85..35ec92004 100644 --- a/blog/2022/12/13/latest-blog-posts-on-tezos.html +++ b/blog/2022/12/13/latest-blog-posts-on-tezos.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2023/01/24/current-verification-efforts.html b/blog/2023/01/24/current-verification-efforts.html index 8efb713b1..91b533ce2 100644 --- a/blog/2023/01/24/current-verification-efforts.html +++ b/blog/2023/01/24/current-verification-efforts.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2023/04/26/representation-of-rust-methods-in-coq.html b/blog/2023/04/26/representation-of-rust-methods-in-coq.html index 6231b0de6..9c6f5665d 100644 --- a/blog/2023/04/26/representation-of-rust-methods-in-coq.html +++ b/blog/2023/04/26/representation-of-rust-methods-in-coq.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2023/05/28/monad-for-side-effects-in-rust.html b/blog/2023/05/28/monad-for-side-effects-in-rust.html index d0c392de5..22d58fad5 100644 --- a/blog/2023/05/28/monad-for-side-effects-in-rust.html +++ b/blog/2023/05/28/monad-for-side-effects-in-rust.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2023/08/25/trait-representation-in-coq.html b/blog/2023/08/25/trait-representation-in-coq.html index c317f79bb..390bd7167 100644 --- a/blog/2023/08/25/trait-representation-in-coq.html +++ b/blog/2023/08/25/trait-representation-in-coq.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2023/11/08/rust-thir-and-bundled-traits.html b/blog/2023/11/08/rust-thir-and-bundled-traits.html index 532c6d09b..eb67923b9 100644 --- a/blog/2023/11/08/rust-thir-and-bundled-traits.html +++ b/blog/2023/11/08/rust-thir-and-bundled-traits.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2023/11/26/rust-function-body.html b/blog/2023/11/26/rust-function-body.html index 194e63606..4536b8888 100644 --- a/blog/2023/11/26/rust-function-body.html +++ b/blog/2023/11/26/rust-function-body.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2023/12/13/rust-verify-erc-20-smart-contract.html b/blog/2023/12/13/rust-verify-erc-20-smart-contract.html index 8ef352585..30bc08301 100644 --- a/blog/2023/12/13/rust-verify-erc-20-smart-contract.html +++ b/blog/2023/12/13/rust-verify-erc-20-smart-contract.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/01/04/rust-translating-match.html b/blog/2024/01/04/rust-translating-match.html index 75392a825..69e98b708 100644 --- a/blog/2024/01/04/rust-translating-match.html +++ b/blog/2024/01/04/rust-translating-match.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/01/18/update-coq-of-rust.html b/blog/2024/01/18/update-coq-of-rust.html index 8b20e0019..92524eb92 100644 --- a/blog/2024/01/18/update-coq-of-rust.html +++ b/blog/2024/01/18/update-coq-of-rust.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/02/02/formal-verification-for-aleph-zero.html b/blog/2024/02/02/formal-verification-for-aleph-zero.html index 46c68c318..b26d53ac5 100644 --- a/blog/2024/02/02/formal-verification-for-aleph-zero.html +++ b/blog/2024/02/02/formal-verification-for-aleph-zero.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/02/14/experiment-coq-of-hs.html b/blog/2024/02/14/experiment-coq-of-hs.html index dcc7ad8dc..acfb97f0f 100644 --- a/blog/2024/02/14/experiment-coq-of-hs.html +++ b/blog/2024/02/14/experiment-coq-of-hs.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/02/22/journey-coq-of-go.html b/blog/2024/02/22/journey-coq-of-go.html index 52912b260..68a38fa85 100644 --- a/blog/2024/02/22/journey-coq-of-go.html +++ b/blog/2024/02/22/journey-coq-of-go.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/02/29/improvements-rust-translation.html b/blog/2024/02/29/improvements-rust-translation.html index 3defbbc88..f0e83aebc 100644 --- a/blog/2024/02/29/improvements-rust-translation.html +++ b/blog/2024/02/29/improvements-rust-translation.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/03/08/improvements-rust-translation-part-2.html b/blog/2024/03/08/improvements-rust-translation-part-2.html index c21c7a30a..7826f7fc0 100644 --- a/blog/2024/03/08/improvements-rust-translation-part-2.html +++ b/blog/2024/03/08/improvements-rust-translation-part-2.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/03/22/improvements-rust-translation-part-3.html b/blog/2024/03/22/improvements-rust-translation-part-3.html index de7a40e49..0439e398b 100644 --- a/blog/2024/03/22/improvements-rust-translation-part-3.html +++ b/blog/2024/03/22/improvements-rust-translation-part-3.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/04/03/monadic-notation-for-rust-translation.html b/blog/2024/04/03/monadic-notation-for-rust-translation.html index 703e8e39e..8aae3a4a4 100644 --- a/blog/2024/04/03/monadic-notation-for-rust-translation.html +++ b/blog/2024/04/03/monadic-notation-for-rust-translation.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/04/26/translation-core-alloc-crates.html b/blog/2024/04/26/translation-core-alloc-crates.html index a5c2f538e..114852b57 100644 --- a/blog/2024/04/26/translation-core-alloc-crates.html +++ b/blog/2024/04/26/translation-core-alloc-crates.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/05/10/translation-of-python-code.html b/blog/2024/05/10/translation-of-python-code.html index df998ddd2..516391d15 100644 --- a/blog/2024/05/10/translation-of-python-code.html +++ b/blog/2024/05/10/translation-of-python-code.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/05/14/translation-of-python-code-simulations.html b/blog/2024/05/14/translation-of-python-code-simulations.html index 0f71614d0..ea7ab0a5a 100644 --- a/blog/2024/05/14/translation-of-python-code-simulations.html +++ b/blog/2024/05/14/translation-of-python-code-simulations.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/05/22/translation-of-python-code-simulations-from-trace.html b/blog/2024/05/22/translation-of-python-code-simulations-from-trace.html index b138d5ae9..34997a2f5 100644 --- a/blog/2024/05/22/translation-of-python-code-simulations-from-trace.html +++ b/blog/2024/05/22/translation-of-python-code-simulations-from-trace.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/06/05/software-correctness-from-first-principles.html b/blog/2024/06/05/software-correctness-from-first-principles.html index 6abad9ba1..88f27d718 100644 --- a/blog/2024/06/05/software-correctness-from-first-principles.html +++ b/blog/2024/06/05/software-correctness-from-first-principles.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/06/28/coq-of-solidity-1.html b/blog/2024/06/28/coq-of-solidity-1.html index 5778c6509..feef9a6ee 100644 --- a/blog/2024/06/28/coq-of-solidity-1.html +++ b/blog/2024/06/28/coq-of-solidity-1.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/08/07/coq-of-solidity-2.html b/blog/2024/08/07/coq-of-solidity-2.html index 92976a292..b767da6e3 100644 --- a/blog/2024/08/07/coq-of-solidity-2.html +++ b/blog/2024/08/07/coq-of-solidity-2.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/08/12/coq-of-solidity-3.html b/blog/2024/08/12/coq-of-solidity-3.html index d5b6c5fe7..bd56bf5a7 100644 --- a/blog/2024/08/12/coq-of-solidity-3.html +++ b/blog/2024/08/12/coq-of-solidity-3.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/08/13/coq-of-solidity-4.html b/blog/2024/08/13/coq-of-solidity-4.html index d3b412c23..e9a1b0aef 100644 --- a/blog/2024/08/13/coq-of-solidity-4.html +++ b/blog/2024/08/13/coq-of-solidity-4.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/08/19/verification-move-sui-type-checker-1.html b/blog/2024/08/19/verification-move-sui-type-checker-1.html index 5fb2b2ed4..82e387a38 100644 --- a/blog/2024/08/19/verification-move-sui-type-checker-1.html +++ b/blog/2024/08/19/verification-move-sui-type-checker-1.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/10/13/class-what-we-do.html b/blog/2024/10/13/class-what-we-do.html index 7e58fffd5..f83fe33c9 100644 --- a/blog/2024/10/13/class-what-we-do.html +++ b/blog/2024/10/13/class-what-we-do.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/10/14/verification-move-sui-type-checker-2.html b/blog/2024/10/14/verification-move-sui-type-checker-2.html index 01b71e60a..d29ff9ef0 100644 --- a/blog/2024/10/14/verification-move-sui-type-checker-2.html +++ b/blog/2024/10/14/verification-move-sui-type-checker-2.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/10/15/verification-move-sui-type-checker-3.html b/blog/2024/10/15/verification-move-sui-type-checker-3.html index fe2c4dc6d..280729e1b 100644 --- a/blog/2024/10/15/verification-move-sui-type-checker-3.html +++ b/blog/2024/10/15/verification-move-sui-type-checker-3.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/10/16/coq-of-solidity-enhanced-version-1.html b/blog/2024/10/16/coq-of-solidity-enhanced-version-1.html index 56710d64a..824290692 100644 --- a/blog/2024/10/16/coq-of-solidity-enhanced-version-1.html +++ b/blog/2024/10/16/coq-of-solidity-enhanced-version-1.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/10/21/verification-smooth-library-1.html b/blog/2024/10/21/verification-smooth-library-1.html index a73f94f02..5f099fb53 100644 --- a/blog/2024/10/21/verification-smooth-library-1.html +++ b/blog/2024/10/21/verification-smooth-library-1.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/10/22/what-we-bring-to-you.html b/blog/2024/10/22/what-we-bring-to-you.html index 5ecfa842d..e9bd6b8fb 100644 --- a/blog/2024/10/22/what-we-bring-to-you.html +++ b/blog/2024/10/22/what-we-bring-to-you.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/10/28/verification-smooth-library-2.html b/blog/2024/10/28/verification-smooth-library-2.html index 84d078250..6f0cb9305 100644 --- a/blog/2024/10/28/verification-smooth-library-2.html +++ b/blog/2024/10/28/verification-smooth-library-2.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/11/01/tool-for-noir-1.html b/blog/2024/11/01/tool-for-noir-1.html index ccdaee927..c5e9b6cf6 100644 --- a/blog/2024/11/01/tool-for-noir-1.html +++ b/blog/2024/11/01/tool-for-noir-1.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/11/14/sui-move-checker-abstract-stack.html b/blog/2024/11/14/sui-move-checker-abstract-stack.html index 48270d201..7e85b84e5 100644 --- a/blog/2024/11/14/sui-move-checker-abstract-stack.html +++ b/blog/2024/11/14/sui-move-checker-abstract-stack.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/11/15/tool-for-noir-2.html b/blog/2024/11/15/tool-for-noir-2.html index 2b8ad538a..cb03a0f0b 100644 --- a/blog/2024/11/15/tool-for-noir-2.html +++ b/blog/2024/11/15/tool-for-noir-2.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/12/20/translation-of-circom-to-coq.html b/blog/2024/12/20/translation-of-circom-to-coq.html index be4c6058b..866d9487d 100644 --- a/blog/2024/12/20/translation-of-circom-to-coq.html +++ b/blog/2024/12/20/translation-of-circom-to-coq.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/12/20/what-is-formal-verification-of-smart-contracts.html b/blog/2024/12/20/what-is-formal-verification-of-smart-contracts.html index 59c9652d8..a473231ba 100644 --- a/blog/2024/12/20/what-is-formal-verification-of-smart-contracts.html +++ b/blog/2024/12/20/what-is-formal-verification-of-smart-contracts.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2024/12/26/mutually-recursive-functions-with-notation.html b/blog/2024/12/26/mutually-recursive-functions-with-notation.html index 40c6324be..3216185c3 100644 --- a/blog/2024/12/26/mutually-recursive-functions-with-notation.html +++ b/blog/2024/12/26/mutually-recursive-functions-with-notation.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2025/01/06/annotating-what-we-are-doing.html b/blog/2025/01/06/annotating-what-we-are-doing.html index 6159f5b00..0f060fa5e 100644 --- a/blog/2025/01/06/annotating-what-we-are-doing.html +++ b/blog/2025/01/06/annotating-what-we-are-doing.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2025/01/13/verification-one-instruction-sui.html b/blog/2025/01/13/verification-one-instruction-sui.html index 75c955cda..e6e86487c 100644 --- a/blog/2025/01/13/verification-one-instruction-sui.html +++ b/blog/2025/01/13/verification-one-instruction-sui.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2025/01/21/designing-a-coding-assistant-for-rocq.html b/blog/2025/01/21/designing-a-coding-assistant-for-rocq.html index c7f1b9f86..e1e894190 100644 --- a/blog/2025/01/21/designing-a-coding-assistant-for-rocq.html +++ b/blog/2025/01/21/designing-a-coding-assistant-for-rocq.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2025/01/30/links-for-rust-in-rocq.html b/blog/2025/01/30/links-for-rust-in-rocq.html index 5481292fe..9ff2761c6 100644 --- a/blog/2025/01/30/links-for-rust-in-rocq.html +++ b/blog/2025/01/30/links-for-rust-in-rocq.html @@ -11,7 +11,7 @@ - + diff --git a/blog/2025/02/05/links-for-rust-in-rocq-2.html b/blog/2025/02/05/links-for-rust-in-rocq-2.html index 42e68c719..aa9daebcb 100644 --- a/blog/2025/02/05/links-for-rust-in-rocq-2.html +++ b/blog/2025/02/05/links-for-rust-in-rocq-2.html @@ -11,7 +11,7 @@ - + diff --git a/blog/archive.html b/blog/archive.html index c8f038755..5b9f46601 100644 --- a/blog/archive.html +++ b/blog/archive.html @@ -11,7 +11,7 @@ - + diff --git a/blog/page/2.html b/blog/page/2.html index 7452de936..249fe8abf 100644 --- a/blog/page/2.html +++ b/blog/page/2.html @@ -11,7 +11,7 @@ - + diff --git a/blog/page/3.html b/blog/page/3.html index b231c3e1b..8cbab6c5a 100644 --- a/blog/page/3.html +++ b/blog/page/3.html @@ -11,7 +11,7 @@ - + diff --git a/blog/page/4.html b/blog/page/4.html index e3cd69c7c..20db6b587 100644 --- a/blog/page/4.html +++ b/blog/page/4.html @@ -11,7 +11,7 @@ - + diff --git a/blog/page/5.html b/blog/page/5.html index 69aa25dd5..854fd74af 100644 --- a/blog/page/5.html +++ b/blog/page/5.html @@ -11,7 +11,7 @@ - + diff --git a/blog/page/6.html b/blog/page/6.html index d419b8e76..8a5458a9c 100644 --- a/blog/page/6.html +++ b/blog/page/6.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags.html b/blog/tags.html index b164e2f30..fbbc10c63 100644 --- a/blog/tags.html +++ b/blog/tags.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/4-14.html b/blog/tags/4-14.html index e46a0ccba..069ca0300 100644 --- a/blog/tags/4-14.html +++ b/blog/tags/4-14.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/ai.html b/blog/tags/ai.html index 2f7d5c799..c1d6addee 100644 --- a/blog/tags/ai.html +++ b/blog/tags/ai.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/aleph-zero.html b/blog/tags/aleph-zero.html index 8b4d2430b..a421aad1e 100644 --- a/blog/tags/aleph-zero.html +++ b/blog/tags/aleph-zero.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/alloc.html b/blog/tags/alloc.html index a268139be..e4da13cff 100644 --- a/blog/tags/alloc.html +++ b/blog/tags/alloc.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/audit.html b/blog/tags/audit.html index c4978a1ef..40fc2289c 100644 --- a/blog/tags/audit.html +++ b/blog/tags/audit.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/circom.html b/blog/tags/circom.html index 3b4817aee..173986cf2 100644 --- a/blog/tags/circom.html +++ b/blog/tags/circom.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/circuits.html b/blog/tags/circuits.html index f1c02a018..231b3d75e 100644 --- a/blog/tags/circuits.html +++ b/blog/tags/circuits.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/coq-of-go.html b/blog/tags/coq-of-go.html index 0938a584e..c95fa06b3 100644 --- a/blog/tags/coq-of-go.html +++ b/blog/tags/coq-of-go.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/coq-of-hs.html b/blog/tags/coq-of-hs.html index b59373c39..814ea35eb 100644 --- a/blog/tags/coq-of-hs.html +++ b/blog/tags/coq-of-hs.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/coq-of-ocaml.html b/blog/tags/coq-of-ocaml.html index 39922db04..784f77c7f 100644 --- a/blog/tags/coq-of-ocaml.html +++ b/blog/tags/coq-of-ocaml.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/coq-of-python.html b/blog/tags/coq-of-python.html index 68fa68b36..8cfd03377 100644 --- a/blog/tags/coq-of-python.html +++ b/blog/tags/coq-of-python.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/coq-of-rust.html b/blog/tags/coq-of-rust.html index 83233e882..a54ffb160 100644 --- a/blog/tags/coq-of-rust.html +++ b/blog/tags/coq-of-rust.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/coq-of-rust/page/2.html b/blog/tags/coq-of-rust/page/2.html index 103fe157a..f55fc0c89 100644 --- a/blog/tags/coq-of-rust/page/2.html +++ b/blog/tags/coq-of-rust/page/2.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/coq-tezos-of-ocaml.html b/blog/tags/coq-tezos-of-ocaml.html index b150fe92f..aadd6663f 100644 --- a/blog/tags/coq-tezos-of-ocaml.html +++ b/blog/tags/coq-tezos-of-ocaml.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/coq.html b/blog/tags/coq.html index 370a637f7..0d5c7400d 100644 --- a/blog/tags/coq.html +++ b/blog/tags/coq.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/coq/page/2.html b/blog/tags/coq/page/2.html index f19163fff..4db664888 100644 --- a/blog/tags/coq/page/2.html +++ b/blog/tags/coq/page/2.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/coq/page/3.html b/blog/tags/coq/page/3.html index b99b218b7..f53e5af9b 100644 --- a/blog/tags/coq/page/3.html +++ b/blog/tags/coq/page/3.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/core.html b/blog/tags/core.html index bfe1c22a8..c734b75ad 100644 --- a/blog/tags/core.html +++ b/blog/tags/core.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/data-encoding.html b/blog/tags/data-encoding.html index 66f5d6a0c..033c2e86b 100644 --- a/blog/tags/data-encoding.html +++ b/blog/tags/data-encoding.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/effects.html b/blog/tags/effects.html index 83a70b49c..50199a22f 100644 --- a/blog/tags/effects.html +++ b/blog/tags/effects.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/elliptic-curves.html b/blog/tags/elliptic-curves.html index 47f78b017..484ce0e54 100644 --- a/blog/tags/elliptic-curves.html +++ b/blog/tags/elliptic-curves.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/erc-20.html b/blog/tags/erc-20.html index 5efc05886..67bf8d1e0 100644 --- a/blog/tags/erc-20.html +++ b/blog/tags/erc-20.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/ethereum.html b/blog/tags/ethereum.html index f41110864..37ef0659d 100644 --- a/blog/tags/ethereum.html +++ b/blog/tags/ethereum.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/example.html b/blog/tags/example.html index 6f1379dab..824655f6e 100644 --- a/blog/tags/example.html +++ b/blog/tags/example.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/first-principles.html b/blog/tags/first-principles.html index 9a68899e1..37e7b0c88 100644 --- a/blog/tags/first-principles.html +++ b/blog/tags/first-principles.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/formal-verification.html b/blog/tags/formal-verification.html index 306b690fc..b738334db 100644 --- a/blog/tags/formal-verification.html +++ b/blog/tags/formal-verification.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/go.html b/blog/tags/go.html index 073e32e6e..303b39b5e 100644 --- a/blog/tags/go.html +++ b/blog/tags/go.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/haskell.html b/blog/tags/haskell.html index e10500ef0..d9f3efadc 100644 --- a/blog/tags/haskell.html +++ b/blog/tags/haskell.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/hir.html b/blog/tags/hir.html index 54e918f6f..682eec3fa 100644 --- a/blog/tags/hir.html +++ b/blog/tags/hir.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/ink.html b/blog/tags/ink.html index b4bad3a69..1cd7bef0f 100644 --- a/blog/tags/ink.html +++ b/blog/tags/ink.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/interactive-theorem-proving.html b/blog/tags/interactive-theorem-proving.html index 239b2a807..6ab046de1 100644 --- a/blog/tags/interactive-theorem-proving.html +++ b/blog/tags/interactive-theorem-proving.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/links.html b/blog/tags/links.html index 6d872287c..9c7c3aa2f 100644 --- a/blog/tags/links.html +++ b/blog/tags/links.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/llm.html b/blog/tags/llm.html index 49e5a2256..497d034d1 100644 --- a/blog/tags/llm.html +++ b/blog/tags/llm.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/loops.html b/blog/tags/loops.html index 024a2cd5a..de89371b0 100644 --- a/blog/tags/loops.html +++ b/blog/tags/loops.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/meetup.html b/blog/tags/meetup.html index b22bb592a..51aeca177 100644 --- a/blog/tags/meetup.html +++ b/blog/tags/meetup.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/mi-cho-coq.html b/blog/tags/mi-cho-coq.html index 491ea81cd..a74753dcf 100644 --- a/blog/tags/mi-cho-coq.html +++ b/blog/tags/mi-cho-coq.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/monad.html b/blog/tags/monad.html index 1299c955e..a512433fe 100644 --- a/blog/tags/monad.html +++ b/blog/tags/monad.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/move.html b/blog/tags/move.html index 7ea48ecc5..4b8ec8dcc 100644 --- a/blog/tags/move.html +++ b/blog/tags/move.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/mutations.html b/blog/tags/mutations.html index 7fc90dd25..0028cb47b 100644 --- a/blog/tags/mutations.html +++ b/blog/tags/mutations.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/mutual.html b/blog/tags/mutual.html index f6eb4db4a..12844ccdd 100644 --- a/blog/tags/mutual.html +++ b/blog/tags/mutual.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/noir.html b/blog/tags/noir.html index 313982a42..66d04a73f 100644 --- a/blog/tags/noir.html +++ b/blog/tags/noir.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/notation.html b/blog/tags/notation.html index 54a288409..be7f507df 100644 --- a/blog/tags/notation.html +++ b/blog/tags/notation.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/o-caml.html b/blog/tags/o-caml.html index b4996469f..be54803d0 100644 --- a/blog/tags/o-caml.html +++ b/blog/tags/o-caml.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/ocaml.html b/blog/tags/ocaml.html index ffd9f159d..317281621 100644 --- a/blog/tags/ocaml.html +++ b/blog/tags/ocaml.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/python.html b/blog/tags/python.html index 27bc0afda..e36a8f96e 100644 --- a/blog/tags/python.html +++ b/blog/tags/python.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/recursion.html b/blog/tags/recursion.html index 663ff7a37..19d59f0b5 100644 --- a/blog/tags/recursion.html +++ b/blog/tags/recursion.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/rust.html b/blog/tags/rust.html index cf5f254be..13f1482cf 100644 --- a/blog/tags/rust.html +++ b/blog/tags/rust.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/rust/page/2.html b/blog/tags/rust/page/2.html index 9e0b8d071..6ce125f44 100644 --- a/blog/tags/rust/page/2.html +++ b/blog/tags/rust/page/2.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/rust/page/3.html b/blog/tags/rust/page/3.html index a91f8ab44..4b6213244 100644 --- a/blog/tags/rust/page/3.html +++ b/blog/tags/rust/page/3.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/security.html b/blog/tags/security.html index ba85071c2..b551828c4 100644 --- a/blog/tags/security.html +++ b/blog/tags/security.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/side-effects.html b/blog/tags/side-effects.html index 94d86513a..3de78c901 100644 --- a/blog/tags/side-effects.html +++ b/blog/tags/side-effects.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/simulation.html b/blog/tags/simulation.html index 1b72dfe0c..de03b1665 100644 --- a/blog/tags/simulation.html +++ b/blog/tags/simulation.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/simulations.html b/blog/tags/simulations.html index b0cca96de..26a43abea 100644 --- a/blog/tags/simulations.html +++ b/blog/tags/simulations.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/smart-contract.html b/blog/tags/smart-contract.html index 6d51d98e1..1956ef046 100644 --- a/blog/tags/smart-contract.html +++ b/blog/tags/smart-contract.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/software-correctness.html b/blog/tags/software-correctness.html index fb50a8a74..766aa218e 100644 --- a/blog/tags/software-correctness.html +++ b/blog/tags/software-correctness.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/solidity.html b/blog/tags/solidity.html index 3044684d5..32c53ef4c 100644 --- a/blog/tags/solidity.html +++ b/blog/tags/solidity.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/sui.html b/blog/tags/sui.html index 67ea6681b..3e7a9db28 100644 --- a/blog/tags/sui.html +++ b/blog/tags/sui.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/tezos.html b/blog/tags/tezos.html index 1316ca74c..879a9e736 100644 --- a/blog/tags/tezos.html +++ b/blog/tags/tezos.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/thir.html b/blog/tags/thir.html index 8124062b9..31c5f91d9 100644 --- a/blog/tags/thir.html +++ b/blog/tags/thir.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/trace.html b/blog/tags/trace.html index ad83be3ad..9f0bead92 100644 --- a/blog/tags/trace.html +++ b/blog/tags/trace.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/trait.html b/blog/tags/trait.html index 4c9aa0301..f9b3cf81b 100644 --- a/blog/tags/trait.html +++ b/blog/tags/trait.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/translation.html b/blog/tags/translation.html index d4ee49115..944dce05c 100644 --- a/blog/tags/translation.html +++ b/blog/tags/translation.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/type-checker.html b/blog/tags/type-checker.html index c697758a9..876a5b9bd 100644 --- a/blog/tags/type-checker.html +++ b/blog/tags/type-checker.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/type-script.html b/blog/tags/type-script.html index 5a84d71f3..3269271fc 100644 --- a/blog/tags/type-script.html +++ b/blog/tags/type-script.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/welcome.html b/blog/tags/welcome.html index 3f5b413d0..2e59cd62a 100644 --- a/blog/tags/welcome.html +++ b/blog/tags/welcome.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/yul.html b/blog/tags/yul.html index 909242c17..2efe7cf8a 100644 --- a/blog/tags/yul.html +++ b/blog/tags/yul.html @@ -11,7 +11,7 @@ - + diff --git a/blog/tags/zero-knowledge.html b/blog/tags/zero-knowledge.html index 317e8c1be..b3443c97c 100644 --- a/blog/tags/zero-knowledge.html +++ b/blog/tags/zero-knowledge.html @@ -11,7 +11,7 @@ - + diff --git a/docs/audit.html b/docs/audit.html index 2a7570630..8264ab23f 100644 --- a/docs/audit.html +++ b/docs/audit.html @@ -11,7 +11,7 @@ - + diff --git a/docs/company/about.html b/docs/company/about.html index 0f0ebf315..857e29727 100644 --- a/docs/company/about.html +++ b/docs/company/about.html @@ -11,7 +11,7 @@ - + diff --git a/docs/company/careers.html b/docs/company/careers.html index cb2fc9ab4..1c04ddc42 100644 --- a/docs/company/careers.html +++ b/docs/company/careers.html @@ -3,7 +3,7 @@ -πŸ§‘β€πŸ’Ό Careers | Formal Land +πŸ§‘β€πŸ’Ό Careers | Formal Land @@ -11,16 +11,12 @@ - +

πŸ§‘β€πŸ’Ό Careers

-
info

Our team is currently complete.

-

If you are knowledgeable in functional programming / theorem provers and want to work with us, contact us. We provide positions in Paris or remote.

-
Content
Links
More
Copyright Β© 2025 Formal Land (Arae SARL), Paris
Formal verification for everyday-life applications πŸŒ²
diff --git a/docs/company/claims.html b/docs/company/claims.html index 1016c5b69..7670e6a08 100644 --- a/docs/company/claims.html +++ b/docs/company/claims.html @@ -11,7 +11,7 @@ - + diff --git a/docs/company/intro.html b/docs/company/intro.html index 6c4fdb761..2ab227675 100644 --- a/docs/company/intro.html +++ b/docs/company/intro.html @@ -11,7 +11,7 @@ - + diff --git a/docs/company/maps.html b/docs/company/maps.html index 5e1f7844b..29995cebb 100644 --- a/docs/company/maps.html +++ b/docs/company/maps.html @@ -11,7 +11,7 @@ - + diff --git a/docs/company/press.html b/docs/company/press.html index bb50654ec..5d7c9ccdc 100644 --- a/docs/company/press.html +++ b/docs/company/press.html @@ -11,7 +11,7 @@ - + diff --git a/docs/learn/start.html b/docs/learn/start.html index 8b038fc23..def2259f5 100644 --- a/docs/learn/start.html +++ b/docs/learn/start.html @@ -11,7 +11,7 @@ - + diff --git a/docs/services/ocaml-development.html b/docs/services/ocaml-development.html index 4b7308147..8947b2e2c 100644 --- a/docs/services/ocaml-development.html +++ b/docs/services/ocaml-development.html @@ -11,7 +11,7 @@ - + diff --git a/docs/services/rust-development.html b/docs/services/rust-development.html index 7344f6596..89460e0be 100644 --- a/docs/services/rust-development.html +++ b/docs/services/rust-development.html @@ -11,7 +11,7 @@ - + diff --git a/docs/services/solidity-development.html b/docs/services/solidity-development.html index 2a1682f48..c92446a0b 100644 --- a/docs/services/solidity-development.html +++ b/docs/services/solidity-development.html @@ -11,7 +11,7 @@ - + diff --git a/docs/services/typescript-development.html b/docs/services/typescript-development.html index 6cd5a5be5..219801965 100644 --- a/docs/services/typescript-development.html +++ b/docs/services/typescript-development.html @@ -11,7 +11,7 @@ - + diff --git a/docs/tools/coq-of-noir/introduction.html b/docs/tools/coq-of-noir/introduction.html index b28eefdb2..7f7db75e8 100644 --- a/docs/tools/coq-of-noir/introduction.html +++ b/docs/tools/coq-of-noir/introduction.html @@ -11,7 +11,7 @@ - + diff --git a/docs/tools/coq-of-ocaml/cookbook.html b/docs/tools/coq-of-ocaml/cookbook.html index a8983ca50..ca413dd5b 100644 --- a/docs/tools/coq-of-ocaml/cookbook.html +++ b/docs/tools/coq-of-ocaml/cookbook.html @@ -11,7 +11,7 @@ - + diff --git a/docs/tools/coq-of-ocaml/install.html b/docs/tools/coq-of-ocaml/install.html index 920a34931..930b056ef 100644 --- a/docs/tools/coq-of-ocaml/install.html +++ b/docs/tools/coq-of-ocaml/install.html @@ -11,7 +11,7 @@ - + diff --git a/docs/tools/coq-of-ocaml/introduction.html b/docs/tools/coq-of-ocaml/introduction.html index ca74f28ac..f8c35da2e 100644 --- a/docs/tools/coq-of-ocaml/introduction.html +++ b/docs/tools/coq-of-ocaml/introduction.html @@ -11,7 +11,7 @@ - + diff --git a/docs/tools/coq-of-ocaml/language.html b/docs/tools/coq-of-ocaml/language.html index 38dd1b6d0..950236472 100644 --- a/docs/tools/coq-of-ocaml/language.html +++ b/docs/tools/coq-of-ocaml/language.html @@ -11,7 +11,7 @@ - + diff --git a/docs/tools/coq-of-ocaml/language/gadts.html b/docs/tools/coq-of-ocaml/language/gadts.html index 847546410..eacfac0fc 100644 --- a/docs/tools/coq-of-ocaml/language/gadts.html +++ b/docs/tools/coq-of-ocaml/language/gadts.html @@ -11,7 +11,7 @@ - + diff --git a/docs/tools/coq-of-ocaml/language/module-system.html b/docs/tools/coq-of-ocaml/language/module-system.html index 607c084a6..96703e3d8 100644 --- a/docs/tools/coq-of-ocaml/language/module-system.html +++ b/docs/tools/coq-of-ocaml/language/module-system.html @@ -11,7 +11,7 @@ - + diff --git a/docs/tools/coq-of-ocaml/language/ocaml-core.html b/docs/tools/coq-of-ocaml/language/ocaml-core.html index 4311a7b46..7d968aa9a 100644 --- a/docs/tools/coq-of-ocaml/language/ocaml-core.html +++ b/docs/tools/coq-of-ocaml/language/ocaml-core.html @@ -11,7 +11,7 @@ - + diff --git a/docs/tools/coq-of-ocaml/language/type-definitions.html b/docs/tools/coq-of-ocaml/language/type-definitions.html index fc636aa81..8f193c7ea 100644 --- a/docs/tools/coq-of-ocaml/language/type-definitions.html +++ b/docs/tools/coq-of-ocaml/language/type-definitions.html @@ -11,7 +11,7 @@ - + diff --git a/docs/tools/coq-of-ocaml/more.html b/docs/tools/coq-of-ocaml/more.html index 090a578bf..b707e4156 100644 --- a/docs/tools/coq-of-ocaml/more.html +++ b/docs/tools/coq-of-ocaml/more.html @@ -11,7 +11,7 @@ - + diff --git a/docs/tools/coq-of-ocaml/more/examples.html b/docs/tools/coq-of-ocaml/more/examples.html index c90832f04..a9b5ac3b3 100644 --- a/docs/tools/coq-of-ocaml/more/examples.html +++ b/docs/tools/coq-of-ocaml/more/examples.html @@ -11,7 +11,7 @@ - + diff --git a/docs/tools/coq-of-ocaml/more/faq.html b/docs/tools/coq-of-ocaml/more/faq.html index c530f5088..7099bf2e0 100644 --- a/docs/tools/coq-of-ocaml/more/faq.html +++ b/docs/tools/coq-of-ocaml/more/faq.html @@ -11,7 +11,7 @@ - + diff --git a/docs/tools/coq-of-ocaml/options.html b/docs/tools/coq-of-ocaml/options.html index 2e7018d95..089b48614 100644 --- a/docs/tools/coq-of-ocaml/options.html +++ b/docs/tools/coq-of-ocaml/options.html @@ -11,7 +11,7 @@ - + diff --git a/docs/tools/coq-of-ocaml/options/attributes.html b/docs/tools/coq-of-ocaml/options/attributes.html index d70a0db59..7e0c97484 100644 --- a/docs/tools/coq-of-ocaml/options/attributes.html +++ b/docs/tools/coq-of-ocaml/options/attributes.html @@ -11,7 +11,7 @@ - + diff --git a/docs/tools/coq-of-ocaml/options/configuration.html b/docs/tools/coq-of-ocaml/options/configuration.html index 56ec118c7..06902b48c 100644 --- a/docs/tools/coq-of-ocaml/options/configuration.html +++ b/docs/tools/coq-of-ocaml/options/configuration.html @@ -11,7 +11,7 @@ - + diff --git a/docs/tools/coq-of-ocaml/run.html b/docs/tools/coq-of-ocaml/run.html index 41b0cc265..90eda3277 100644 --- a/docs/tools/coq-of-ocaml/run.html +++ b/docs/tools/coq-of-ocaml/run.html @@ -11,7 +11,7 @@ - + diff --git a/docs/tools/coq-of-rust/introduction.html b/docs/tools/coq-of-rust/introduction.html index 7ea8d054e..631c1e367 100644 --- a/docs/tools/coq-of-rust/introduction.html +++ b/docs/tools/coq-of-rust/introduction.html @@ -11,7 +11,7 @@ - + diff --git a/docs/tools/coq-of-solidity/introduction.html b/docs/tools/coq-of-solidity/introduction.html index 2ab25c071..99a1f1d1c 100644 --- a/docs/tools/coq-of-solidity/introduction.html +++ b/docs/tools/coq-of-solidity/introduction.html @@ -11,7 +11,7 @@ - + diff --git a/docs/verification/ocaml.html b/docs/verification/ocaml.html index 49cf780c2..1d4d010da 100644 --- a/docs/verification/ocaml.html +++ b/docs/verification/ocaml.html @@ -11,7 +11,7 @@ - + diff --git a/docs/verification/rust.html b/docs/verification/rust.html index ff8812ed9..b28ec4f99 100644 --- a/docs/verification/rust.html +++ b/docs/verification/rust.html @@ -11,7 +11,7 @@ - + diff --git a/docs/verification/solidity.html b/docs/verification/solidity.html index f04de5827..69f166336 100644 --- a/docs/verification/solidity.html +++ b/docs/verification/solidity.html @@ -11,7 +11,7 @@ - + diff --git a/docs/verification/typescript.html b/docs/verification/typescript.html index bb483573a..63e9f30fe 100644 --- a/docs/verification/typescript.html +++ b/docs/verification/typescript.html @@ -11,7 +11,7 @@ - + diff --git a/index.html b/index.html index 5ca5aa6b4..eae087019 100644 --- a/index.html +++ b/index.html @@ -11,7 +11,7 @@ - +