AI-related laws, standards, and norms are emerging rapidly. However, a lack of shared descriptive concepts and monitoring infrastructure undermine efforts to track, understand, and improve AI governance. We introduce AGORA (the AI Governance and Regulatory Archive), a rigorously compiled and enriched dataset of AI-focused laws and policies encompassing diverse jurisdictions, institutions, and contexts related to AI. AGORA is oriented around an original taxonomy describing risks, potential harms, governance strategies, incentives for compliance, and application domains addressed in AI regulatory documents. At launch, AGORA included data on over 330 instruments, with new entries being added continuously. We describe the manual and automated processes through which these data are systematically compiled, screened, annotated, and validated, enabling deep, efficient, and reliable analysis of the emerging AI governance landscape. The dataset, supporting information, and analyses are available through a public web interface (https://agora.eto.tech) and bulk dataset.

We present verification of a bare-metal server built using diverse implementation techniques and languages against a whole-system input-output specification in terms of machine code, network packets, and mathematical specifications of elliptic-curve cryptography. We used very different formal-reasoning techniques throughout the stack, ranging from computer algebra, symbolic execution, and verification-condition generation to interactive verification of functional programs including compilers for C-like and functional languages. All these component specifications and domain-specific reasoning techniques are defined and justified against common foundations in the Coq proof assistant. Connecting these components is a minimalistic specification style based on functional programs and assertions over simple objects, omnisemantics for program execution, and basic separation logic for memory layout. This design enables us to bring the components together in a top-level correctness theorem that can be audited without understanding or trusting the internal interfaces and tools. Our case study is a simple cryptographic server for flipping of a bit of state through public-key authenticated network messages, and its proof shows total functional correctness including static bounds on memory usage. This paper also describes our experiences with the specific verification tools we build upon, along with detailed analysis of reasons behind the widely varying levels of productivity we experienced between combinations of tools and tasks.