Zarko Milosevic, CTO of Informal Systems, provided a comprehensive update on his organization’s significant contributions to the Cosmos ecosystem, detailing advancements in formal verification, stewardship of the Tendermint Core, and the underlying values driving these innovations. With a background in Byzantine fault tolerance and consensus protocols, Milosevic emphasizes Informal’s commitment to improving the security and scalability of distributed systems, transforming key pillars of society: money, software, and organizations. Informal Systems, which has grown to around sixty people, maintains its core cooperative values while taking on increasing responsibilities, including becoming the steward for the Tendermint Core repository and the Cosmos Hub. Milosevic notes that despite the pressures of rapid growth and new structures like the ICF’s Technical Advisory Board, the company’s mission and vision have only solidified. He states, "values are still there. In terms of like the company mission and vision, I think like that we manage to like even solidify things even more so we are, I would say even more ambitious. So, like the current way we phrase what you're doing at Informal is trying to transform the three major pillar of society... money, software, and organizations." This holistic approach, including a focus on internal governance with methodologies like "workflow," aims to lead by example within the broader Cosmos governance. A major announcement from Milosevic was the open-sourcing of Quint, a new formal specification language designed to make verification tools more accessible and developer-friendly. He highlights that "Quint is important because the challenges of verification tools in our view and our experience are mostly on like adoption and developer friendliness side of thing." Inspired by TLA+, Quint offers a modern programming language-like syntax, similar to Scala or Rust, a command-line interface, a built-in simulator, and integration with Informal’s Apalache model checker. It provides a full type-checking experience with a VS Code plugin, allowing developers to design protocols with the guarantees of formal verification without the steep learning curve traditionally associated with such tools. Quint aims to replace conventional pseudocode in specifications, making them executable, type-checkable, and continually synchronized with implementation. This approach generates "model-based tests" through a language-agnostic format, ensuring consistent testing across different implementations like Go or Rust. Milosevic acknowledges the historical resistance from developers to formal verification, stating, "people hated this and so they were not, although they were able to appreciate the values just the cost of learning and using tools was so high that they were not able and also maintaining it after." He underscores that these tools are not meant to replace human developers but to assist them in building more secure and correct systems. "These tools are here not to replace us but to actually assist people in like hopefully doing their job with more fun and like faster and in more than you know safe and correct way." Quint's language-agnostic nature also allows for seamless integration with frameworks like CosmWasm, reflecting the belief that "it doesn't make sense to separate the two, they need to like co-exist with each other and be in love." Informal Systems has also become the steward of the Tendermint Core consensus engine, signaling a transition to a "new generation of the consensus engine." This shift involves significant changes, particularly with the introduction of ABCI++ (Application Blockchain Interface++). ABCI++ fundamentally alters how the consensus engine and applications interact, enabling greater flexibility and performance. For instance, the `PrepareProposal` API allows applications to modify, delete, or add transactions to a block before it is proposed, while `ProcessProposal` enables applications to validate transactions before participants vote. This prevents "a block full of crap," as Milosevic puts it. Additionally, ABCI++ supports optimistic and parallel execution during consensus progression and introduces experimental `VoteExtensions` for applications to piggyback data on pre-commit messages, facilitating features like native oracles or threshold encryption. These innovations open up numerous new use cases and significantly enhance the usability and performance of state machine applications. Milosevic notes that this is a departure from existing approaches, which typically "were just like pretty much like you know like agreeing on something and then passing it to the applicational level." This new stewardship also comes with a rebranding of Tendermint Core, as Informal has forked the project due to differing visions with All In Bits/Jae Kwon regarding the engine's evolution. Milosevic states, "we are a bit forced to like to fork and rebrand essentially what was the previously considered as Tendermint core and that's something which we have like a new name but we are in a process of like actually essentially doing legal work to properly brand this." Despite this, both Informal and ICF are committed to supporting the project, with Milosevic humorously remarking, "in Cosmos everything is decentralized and full torrent and now we are having given like full torrent implementation of the consensus engine." The team plans to focus on improving QA processes, cleaning up internal interfaces for modularity, and enabling experimentation. Addressing the critical issue of scalability, Milosevic acknowledges that while ABCI++ will improve performance, increasing the number of validators requires further research and changes at various stack levels, particularly in the peer-to-peer layer. He highlights the high operational cost of running Tendermint nodes, which can be prohibitive for "small socially impactful projects." He believes that "if you really want you know to make impact to the society we need to allow people to like be able to use the stuff in a secure and decentralized way but still you know with a reasonable price." Informal’s work on collaborative finance (Cofi) projects also underscores the need for more cost-effective solutions for on-chain community initiatives. Milosevic concludes by expressing his motivation, primarily deriving from working with "brilliant people" at Informal Systems and the impactful ideas they pursue. He finds inspiration in researchers like Fernando Perdone, whose work in distributed systems significantly influences his approach.