🛠 July Latest Dev Update – Building the Core of Tau Net’s TestNet Alpha The team pushed further toward TestNet Alpha by finalizing block creation, improving parsing performance, and developing new algorithms for formula normalization. Highlights: - TestNet Alpha: Block creation, linking, and Merkle root storage completed - SAT Solver: Migration from Z3 to CVC5 unlocked better normalization & satisfiability - Parsing Engine: 60% performance boost + potential new parsing patent - Language R&D: Anti-prenexing normalization & Boolean quantifier elimination spec ready. Ohad has been reviewing the latest temporal logic papers. Tau Net and $AGRS remain far ahead of current academic progress in the field. Timestamps: 00:12 - Karim’s Summary 03:48 - David (Lead Developer) - Successfully switched from Z3 to CVC5, improving overall solver performance. - Completed work on normalization, satisfiability, and interpreter modules with CVC5. - Implemented Ohad’s suggested approach of deferring literal resolution for bit vector equations. - Assisted Umar with code reviews and debugging. 05:36 - Lucca (Tau Language Developer) - Developed the initial specification for an algorithm to eliminate function quantifiers for use in Tau’s table feature. - Integrated it into the anti-prenexing normalization algorithm to handle formulas not covered by CVC5. - Preparing to implement this algorithm now that the pseudo-code is finalized. - Began using Tomáš’s new tree implementation and assisted in resolving its final issues. 08:30 - Andrei Korotkoff (Senior Developer) - Completed testnet alpha milestone for block production and storage, including mempool handling, block linking, Merkle root computation, and database persistence. - This work lays the foundation for the next milestone: persistent chain state based on block history. - Developed a complex load testing tool to simulate Tau interpreter behavior and blockchain dynamics under pointwise revision. 11:20 - Tomáš Klapka (Senior Developer) - Fixed several issues from the tree switch, including negation handling, grammar typos, and type inference errors. - Refactored the parser library to be header-only. - Created Docker support and nightly releases for the TGF tool and parser. - Updated the Tau language to integrate the improved parser. 12:26 - Ohad (Founder & CTO) - Focused on new algorithm design and team collaboration. - Explored domain-independent languages to enhance decision procedures. - Reviewed recent academic papers on temporal logic and confirmed Tau remains ahead of current research.