Understanding how local molecular interactions give rise to global cellular outcomes is a central challenge in computational systems biology. Rule-based modeling frameworks such as Kappa provide a way to specify these interactions compactly as rules, which can be simulated to produce causal ``stories'' explaining how a specified event of interest (EOI) arises. However, even small changes in the conditions of a rule can change these causal structures in ways that are difficult to anticipate. This thesis addresses the question: how do modifications to rules affect the causal stories produced by a model? We propose a novel program synthesis framework that automates the generation and exploration of Kappa programs. First, we construct a grammar specialized to a given program's agent signature, extended with constraints to ensure only valid rules are produced. Second, we introduce a rule modification procedure that systematically adds structural contextual conditions to rules while preserving their core transformations. Together, these techniques allow us to enumerate the space of modified programs and retrieve subsets of this space guided by user-defined specifications over the stories. Our experiments show that the constraints reduce the search space by several orders of magnitude, making exhaustive exploration feasible for small models. Using static analysis tools, we reduce the exploration time by 45\%. We demonstrate how different specifications, such as ensuring EOI reachability, can be used to retrieve a subset of modified programs that satisfy them automatically. Together, this work demonstrates the effectiveness of the program synthesis approach in modeling kappa programs and posing questions about their causal structure.

Achieving consensus in a network is one of the most important performance bottlenecks in distributed computing. This paper takes a look at the existing protocols for achieving Byzantine Reliable Broadcast on asynchronous partially connected networks and how these protocols change to leverage the fact that some nodes have access to Trusted Execution Environments. Modeling some nodes to be completely trusted improves the throughput and reduces latency but the impact changes heavily depending on the placement of these nodes. The second, more realistic approach is having all processes use a local trusted subsystem implemented in a TEE. We show that this reduces the upper bound of faulty nodes from f<N/3 to f<N/2 and reducing the amount of messages sent by up to 64\% (N=30, f=5).