Project Everest's verified TLS stack in F* took ~100 person-years and 1.5M lines of code/proof. Since then, we enlisted agents to build verified TLS 1.3 and crypto implementations in 6 weeks each, and X.509 in 6 hours. In line with similar advances in Lean and Rocq, such experiments highlight three challenges for agentic proof-oriented programming.

1/ How to audit specifications? We leveraged agents to implement and prove 52 CLRS algorithms and data structures in Pulse, the separation logic framework for F*; they initially came with imprecise specs. We introduce Small Proof-Oriented Tests (SPOTs) to expose weaknesses through proven clients. SPOTs, abstraction and ghost state support auditing and strengthening specs, including complexity analysis.

2/ How to prove properties beyond memory safety and functional correctness? We leveraged agents to produce Atlas, a Pulse implementation of TLS 1.3, X.509 and NIST crypto, verified for key agreement. ~500K Pulse lines yield 100K C lines; ~500 theorem lines, rubrics and state-machine specs streamline review. Proven optimizations close the gap with OpenSSL.

3/ How to verify existing code at scale? We introduce PAL, a Proof Annotation Language for C, along with a compiler translating annotated C into Pulse with separation logic specs and proofs. Agents annotate C in place, enabling verification of Linux's loopback driver and Microsoft's MSQUIC.

In regression and classification tasks with tabular datasets, most of the literature on explanation in ML (e.g. SHAP, permutation importance) has focused on predictive attribution: does feature X_i help predict outcome Y? At its heart, predictive attribution captures correlation, not causation. We instead ask a causal question: would manipulating feature X_i change outcome Y? We define a natural quantity to answer this question, the feature intervention effect: Δ_i = E[Y | do(X_i=+1)] − E[Y | do(X_i=−1)]. In general, estimating this quantity from observational data alone would entail strong causal assumptions. We propose FADO (Feature-wise Amortized Do-Operators), an amortized inference method using prior-fitted networks trained on synthetic tabular datasets generated by structural causal models. During training, the synthetic data generating process is known, so we can compute ground truth intervention effects Δ_i, and train a model to predict them at test time from a purely observational tabular dataset. As we demonstrate through extensive experiments, our new causal explainability method is easy to train and provides better explanations under a range of settings for which standard predictive attribution fails, including proxy variables, confounders, colliders, and placebos. We evaluate it on real, synthetic and semi-synthetic datasets, with and without hidden confounders, and compare it to existing predictive attribution methods and state-of-the-art causal inference methods.

As AI agents increasingly engage in high-stakes decision making, it is essential to assess their accountability in ways that are both fair and interpretable. This involves explaining expected or realized outcomes of multi-agent systems and attributing responsibility for those outcomes to the participating agents. Addressing these challenges is key to fostering societal trust and easing the adoption of AI decision makers. This thesis investigates accountability in multi-agent sequential decision making. We develop methods to attribute responsibility for observed outcomes and overall system performance, design efficient approximation algorithms for otherwise intractable attribution problems, and introduce causal tools to explain how agents’ decisions influence outcomes. Together, these contributions establish theoretical foundations and practical tools for accountable decision making, drawing on and integrating insights from causality, multi-agent reinforcement learning and game theory.