About

Nate Foster is an adjunct professor of computer science at Cornell University and a visiting researcher at Jane Street. He currently serves as vice chair of DARPA's Information Science and Technology (ISAT) study group and as chair of the P4 Language Governing Board. Foster's research aims to develop languages and tools that facilitate the building of secure and reliable systems. His current work focuses on the design and implementation of languages and tools for programmable networks. His past research includes work on bidirectional languages (also known as lenses), database query languages, data provenance, type systems, mechanized proof, and formal semantics. Foster holds a Ph.D. in computer and information science from the University of Pennsylvania, a Master of Philosophy in history and philosophy of science from Cambridge University, and a B.A. in computer science from Williams College. He is an ACM Fellow and has received numerous awards including a Sloan Research Fellowship, an NSF CAREER Award, the SIGPLAN Robin Milner Award, and the SIGCOMM Rising Star Award.

Research topics

• Computer Science
• Programming language
• Operating system
• Computer Security
• Distributed computing
• Artificial Intelligence
• Discrete mathematics
• Mathematics
• Computer network
• Computer architecture
• Theoretical computer science

Selected publications

• Weighted NetKAT: A Programming Language For Quantitative Network Verification

  ArXiv.org · 2026-04-15

  articleOpen access

  We introduce weighted NetKAT, a domain-specific language for modeling and verifying quantitative network properties. The language is parametric on a semiring, enabling the treatment of a wide range of quantities in a uniform way. We provide a denotational semantics and an equivalent operational semantics, the latter based on a novel model of weighted NetKAT automata (WNKA) capturing the stateful behavior of our language. With WNKA, we obtain a class of generic decision procedures for reasoning about quantitative safety and reachability in a fully automatic way, even in the presence of possibly unbounded iteration. We demonstrate the applicability of our framework in a case study using Internet2's Abilene network as the underlying topology.

  PublisherOA PDF

• Weighted NetKAT: A Programming Language For Quantitative Network Verification

  arXiv (Cornell University) · 2026-04-15

  preprintOpen access

  We introduce weighted NetKAT, a domain-specific language for modeling and verifying quantitative network properties. The language is parametric on a semiring, enabling the treatment of a wide range of quantities in a uniform way. We provide a denotational semantics and an equivalent operational semantics, the latter based on a novel model of weighted NetKAT automata (WNKA) capturing the stateful behavior of our language. With WNKA, we obtain a class of generic decision procedures for reasoning about quantitative safety and reachability in a fully automatic way, even in the presence of possibly unbounded iteration. We demonstrate the applicability of our framework in a case study using Internet2's Abilene network as the underlying topology.

  PublisherDOI

• Lightweight Hypervisor Verification: Putting the Hardware Burger on a Diet

  2025-05-14 · 1 citations

  articleOpen access

  Hypervisors are an essential part of our computing infrastructure, yet ensuring their correctness remains a significant challenge for the community. While several hypervisors have been formally verified using traditional methods, they have typically required a huge effort and significant input from verification experts. With the increasing diversity of hypervisors, driven by open hardware and custom ISAs, there is a growing need for more accessible approaches that can be used by non-experts.

  PublisherOA PDFDOI

• It Takes a Village: Bridging the Gaps between Current and Formal Specifications for Protocols

  ArXiv.org · 2025-09-16

  preprintOpen access

  Formal specifications have numerous benefits for both designers and users of network protocols. They provide clear, unambiguous representations, which are useful as documentation and for testing. They can help reveal disagreements about what a protocol "is" and identify areas where further work is needed to resolve ambiguities or internal inconsistencies. They also provide a foundation for formal reasoning, making it possible to establish important security and correctness guarantees on all inputs and in every environment. Despite these advantages, formal methods are not widely used to design, implement, and validate network protocols today. Instead, Internet protocols are usually described in informal documents, such as IETF Requests for Comments (RFCs) or IEEE standards. These documents primarily consist of lengthy prose descriptions, accompanied by pseudocode, header descriptions, state machine diagrams, and reference implementations which are used for interoperability testing. So, while RFCs and reference implementations were only intended to help guide the social process used by protocol designers, they have evolved into the closest things to formal specifications the Internet community has. In this paper, we discuss the different roles that specifications play in the networking and formal methods communities. We then illustrate the potential benefits of specifying protocols formally, presenting highlights from several recent success stories. Finally, we identify key differences between how formal specifications are understood by the two communities and suggest possible strategies to bridge the gaps.

  PublisherOA PDFDOI

• Active Learning of Symbolic NetKAT Automata

  Proceedings of the ACM on Programming Languages · 2025-06-10

  articleOpen access

  NetKAT is a domain-specific programming language and logic that has been successfully used to specify and verify the behavior of packet-switched networks. This paper develops techniques for automatically learning NetKAT models of unknown networks using active learning. Prior work has explored active learning for a wide range of automata (e.g., deterministic, register, Büchi, timed etc.) and also developed applications, such as validating implementations of network protocols. We present algorithms for learning different types of NetKAT automata, including symbolic automata proposed in recent work. We prove the soundness of these algorithms, build a prototype implementation, and evaluate it on a standard benchmark. Our results highlight the applicability of symbolic NetKAT learning for realistic network configurations and topologies.

  PublisherDOI

• StacKAT: Infinite State Network Verification

  Proceedings of the ACM on Programming Languages · 2025-06-10

  articleOpen access

  We develop StacKAT, a network verification language featuring loops, finite state variables, nondeterminism, and---most importantly---access to a stack with accompanying push and pop operations. By viewing the variables and stack as the (parsed) headers and (to-be-parsed) contents of a network packet, StacKAT can express a wide range of network behaviors including parsing, source routing, and telemetry. These behaviors are difficult or impossible to model using existing languages like NetKAT. We develop a decision procedure for StacKAT program equivalence, based on finite automata. This decision procedure provides the theoretical basis for verifying network-wide properties and is able to provide counterexamples for inequivalent programs. Finally, we provide an axiomatization of StacKAT equivalence and establish its completeness.

  PublisherDOI

• It Takes a Village: Bridging the Gaps between Current and Formal Specifications for Protocols

  Communications of the ACM · 2025-07-23

  article

  Formal specifications have numerous benefits for both designers and users of network protocols. They provide clear, unambiguous representations, which are useful as documentation and for testing. They can help reveal disagreements about what a protocol “is” and identify areas where further work is needed to resolve ambiguities or internal inconsistencies. They also provide a foundation for formal reasoning, making it possible to establish important security and correctness guarantees on all inputs and in every environment. Despite these advantages, formal methods are not widely used to design, implement, and validate network protocols today. Instead, Internet protocols are usually described in informal documents, such as IETF Requests for Comments (RFCs) or IEEE standards. These documents primarily consist of lengthy prose descriptions, accompanied by pseudocode, header descriptions, state machine diagrams, and reference implementations which are used for interoperability testing. So, while RFCs and reference implementations were only intended to help guide the social process used by protocol designers, they have evolved into the closest things to formal specifications the Internet community has. In this paper, we discuss the different roles that specifications play in the networking and formal methods communities. We then illustrate the potential benefits of specifying protocols formally, presenting highlights from several recent success stories. Finally, we identify key differences between how formal specifications are understood by the two communities and suggest possible strategies to bridge the gaps.

  PublisherDOI

• KATch: A Fast Symbolic Verifier for NetKAT

  Proceedings of the ACM on Programming Languages · 2024-06-20 · 8 citations

  preprintOpen access

  We develop new data structures and algorithms for checking verification queries in NetKAT, a domain-specific language for specifying the behavior of network data planes. Our results extend the techniques obtained in prior work on symbolic automata and provide a framework for building efficient and scalable verification tools. We present KATch, an implementation of these ideas in Scala, featuring an extended set of NetKAT operators that are useful for expressing network-wide specifications, and a verification engine that constructs a bisimulation or generates a counter-example showing that none exists. We evaluate the performance of our implementation on real-world and synthetic benchmarks, verifying properties such as reachability and slice isolation, typically returning a result in well under a second, which is orders of magnitude faster than previous approaches. Our advancements underscore NetKAT’s potential as a practical, declarative language for network specification and verification.

  PublisherOA PDFDOI

• Computing Precise Control Interface Specifications

  Proceedings of the ACM on Programming Languages · 2024-10-08

  articleOpen accessSenior author

  Verifying network programs is challenging because of how they divide labor: the control plane computes high level routes through the network and compiles them to device configurations, while the data plane uses these configurations to realize the desired forwarding behavior. In practice, the correctness of the data plane often assumes that the configurations generated by the control plane will satisfy complex specifications. Consequently, validation tools such as program verifiers, runtime monitors, fuzzers, and test-case generators must be aware of these control interface specifications (ci-specs) to avoid raising false alarms. In this paper, we propose the first algorithm for computing precise ci-specs for network data planes. Our specifications are designed to be efficiently monitorable —concretely, checking that a fixed configuration satisfies a ci-spec can be done in polynomial time. Our algorithm, based on modular program instrumentation, quantifier elimination, and a path-based analysis, is more expressive than prior work, and is applicable to practical network programs. We describe an implementation and show that ci-specs computed by our tool are useful for finding real bugs in real-world data plane programs.

  PublisherDOI

• Lenses for Web Data

  2024-03-25 · 13 citations

  articleOpen access

  Putting data on the web typically involves implementing two transformations: one to convert the data into HTML, and another to parse modifications out of interactions with clients. Unfortunately, in current systems, these transformations are usually implemented using two separate functions—an approach that replicates functionality across multiple pieces of code, and makes programs difficult to write, reason about, and maintain. This paper presents a different approach: an abstraction based on formlets that makes it easy to bridge the gap between data stored on a server and values embedded in HTML forms. We introduce formlenses, which combine the advantages of formlets with those of lenses to provide compositional, bidirectional form-based views of Web data. We show that formlenses can be viewed as monoidal functors over lenses, analogously to formlets, which are applicative functors. Finally, we investigate the connection between linearity and bidirectional transformations and describe a translation from a linear pattern syntax into formlens combinators.

  PublisherOA PDFDOI

Frequent coauthors

• Robert Soulé

  32 shared

• Dexter Kozen

  16 shared

• David Walker

  Princeton University

  15 shared

• Hossein Hojjat

  15 shared

• Pavol Černý

  TU Wien

  14 shared

• Jedidiah McClurg

  Colorado State University

  13 shared

• Steffen Smolka

  Google (United States)

  13 shared

• Arjun Guha

  Northeastern University

  13 shared

Awards & honors

• Sloan Research Fellowship
• NSF CAREER Award
• SIGPLAN Robin Milner Award
• SIGCOMM Rising Star Award
• ACM Fellow