From 6aebe6c59466069bb12eaa5e7226d60f232a4031 Mon Sep 17 00:00:00 2001 From: James Chapman Date: Thu, 10 Aug 2023 08:44:22 +0100 Subject: [PATCH 1/4] Javier's info --- blog/2023-07-20-goedel.md | 21 +++++++++++++++++++++ blog/2023-08-04-goedel.md | 18 ++++++++++++++++++ docusaurus.config.js | 1 + 3 files changed, 40 insertions(+) create mode 100644 blog/2023-07-20-goedel.md create mode 100644 blog/2023-08-04-goedel.md diff --git a/blog/2023-07-20-goedel.md b/blog/2023-07-20-goedel.md new file mode 100644 index 0000000000..346a8a6ab2 --- /dev/null +++ b/blog/2023-07-20-goedel.md @@ -0,0 +1,21 @@ +--- +title: Goedel Team Update +slug: 2023-07-20-goedel +authors: jmchapman +tags: [goedel] +hide_table_of_contents: false +--- + +The team works on applied research and consulting in formal methods +that is directly applicable to evidence based engineering in Core Tech +and beyond. + +## High level summary + +## Details + +* Formalization of the chain synchronization mini-protocol in Isabelle + +* Review of the framework for specification and verification of + mini-protocols + diff --git a/blog/2023-08-04-goedel.md b/blog/2023-08-04-goedel.md new file mode 100644 index 0000000000..bc969b12a0 --- /dev/null +++ b/blog/2023-08-04-goedel.md @@ -0,0 +1,18 @@ +--- +title: Goedel Team Update +slug: 2023-07-07-goedel +authors: jmchapman +tags: [goedel] +hide_table_of_contents: false +--- + +The team works on applied research and consulting in formal methods +that is directly applicable to evidence based engineering in Core Tech +and beyond. + +## High level summary + +## Details + +* Review of the framework for specification and verification of + mini-protocols \ No newline at end of file diff --git a/docusaurus.config.js b/docusaurus.config.js index 6f41ff34d6..7a82818352 100644 --- a/docusaurus.config.js +++ b/docusaurus.config.js @@ -97,6 +97,7 @@ const config = { { to: 'tags/cli-api', label: 'Node CLI & API' }, { to: 'quarterly/tags/cli-api-quarterly', label: 'Node CLI & API Quarterly' }, { to: 'tags/crypto', label: 'Crypto' }, + { to: 'tags/goedel', label: 'Goedel' }, ], }, { to: 'archive', label: 'Archive', position: 'right' }, From 7758c066c78ad584beb59234063cae7425ca8e91 Mon Sep 17 00:00:00 2001 From: James Chapman Date: Thu, 10 Aug 2023 09:57:39 +0100 Subject: [PATCH 2/4] Jacob's info --- blog/2023-07-20-goedel.md | 2 ++ blog/2023-08-04-goedel.md | 7 +++++-- 2 files changed, 7 insertions(+), 2 deletions(-) diff --git a/blog/2023-07-20-goedel.md b/blog/2023-07-20-goedel.md index 346a8a6ab2..70b03c9a60 100644 --- a/blog/2023-07-20-goedel.md +++ b/blog/2023-07-20-goedel.md @@ -19,3 +19,5 @@ and beyond. * Review of the framework for specification and verification of mini-protocols +* Started work on porting the DeltaQ framework to a new, more concrete + backend based on piecewise-polynomials \ No newline at end of file diff --git a/blog/2023-08-04-goedel.md b/blog/2023-08-04-goedel.md index bc969b12a0..ea3148fa25 100644 --- a/blog/2023-08-04-goedel.md +++ b/blog/2023-08-04-goedel.md @@ -1,6 +1,6 @@ --- title: Goedel Team Update -slug: 2023-07-07-goedel +slug: 2023-08-04-goedel authors: jmchapman tags: [goedel] hide_table_of_contents: false @@ -15,4 +15,7 @@ and beyond. ## Details * Review of the framework for specification and verification of - mini-protocols \ No newline at end of file + mini-protocols + +* Developed a new internal representation for the DeltaQ algebra that + allows for more modularity in backend implementations \ No newline at end of file From a33d2a5b27795583313a6c66ab16fb82634cd725 Mon Sep 17 00:00:00 2001 From: James Chapman Date: Mon, 14 Aug 2023 14:39:13 +0100 Subject: [PATCH 3/4] update to 20th July update --- blog/2023-07-20-goedel.md | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/blog/2023-07-20-goedel.md b/blog/2023-07-20-goedel.md index 70b03c9a60..d30b00f4ee 100644 --- a/blog/2023-07-20-goedel.md +++ b/blog/2023-07-20-goedel.md @@ -14,9 +14,12 @@ and beyond. ## Details -* Formalization of the chain synchronization mini-protocol in Isabelle +* Formalization of the chain synchronization mini-protocol in the + thorn calculus -* Review of the framework for specification and verification of +* Final pre-publication steps for ICE 2023 papers + +* Developing approach for specification and verification of mini-protocols * Started work on porting the DeltaQ framework to a new, more concrete From d65b234127d6eefcddbeae78f44cc03f334a02c4 Mon Sep 17 00:00:00 2001 From: James Chapman Date: Mon, 14 Aug 2023 14:45:31 +0100 Subject: [PATCH 4/4] updates to 4th August and 20th July --- blog/2023-07-20-goedel.md | 3 +++ blog/2023-08-04-goedel.md | 11 ++++++++--- 2 files changed, 11 insertions(+), 3 deletions(-) diff --git a/blog/2023-07-20-goedel.md b/blog/2023-07-20-goedel.md index d30b00f4ee..812c51e78e 100644 --- a/blog/2023-07-20-goedel.md +++ b/blog/2023-07-20-goedel.md @@ -12,6 +12,9 @@ and beyond. ## High level summary +The team is working on formalising mini protocols, the performance +modelling prototype and also finishing off their ICE papers. + ## Details * Formalization of the chain synchronization mini-protocol in the diff --git a/blog/2023-08-04-goedel.md b/blog/2023-08-04-goedel.md index ea3148fa25..b240fab63a 100644 --- a/blog/2023-08-04-goedel.md +++ b/blog/2023-08-04-goedel.md @@ -12,10 +12,15 @@ and beyond. ## High level summary +The team is formalising mini protocols and also further developing the +performance modelling prototype. + ## Details -* Review of the framework for specification and verification of - mini-protocols +* Developing new framework for specification and verification of + mini-protocols which is closer to the Haskell implementation. * Developed a new internal representation for the DeltaQ algebra that - allows for more modularity in backend implementations \ No newline at end of file + allows for more modularity in backend implementations + +* Discussions regarding the Cardano networking specification \ No newline at end of file