1 Introduction↩︎

Although often overlooked, or treated as a secondary task after a system is implemented, specifications are a critical component in modern software development. A comprehensive specification is the foundation for ensuring that a software artifact matches the intent of the stakeholders, that it has been correctly implemented, and enables clients to use the system without making (risky) assumptions. Specifications become even more critical in the context of agentic software development. Without appropriate structure and information agentic systems quickly start to make erroneous assumptions and generate incorrect code or take dangerous actions.

Would you trust your AI agent to use the API below to make payments from your bank account? In fact even with human level AGI this kind of API has proven [1], [2] to be poorly specified and definitely unsafe!

api transfer(amt: USD, payer: Account, payee: Account);

Addressing the challenges facing software developers today and the new challenges presented by agentic software development requires a shift to an aggressively spec-centered method of software engineering. In this approach, specifications are the primary artifact of the software development process, and from them, flows the implementation, testing, deployment, and interaction with AI agents, data, and other systems. This paper outlines the Bosque API (BAPI) specification ecosystem, consisting of the BAPI specification language, which supports specification of data, behavior, temporal relations, and resources. We also describe tooling to support validation and testing of implementations, automated polyglot runtime interoperation & data quality assurance, along with specialized features for agentic software development.

The BAPI specification language takes the current state-of-the-art for REST API specifications for inspiration, specifically TypeSpec [3] and Smithy [4], and the core ideas that an API specification should be more akin to a programming language than simply a description of a data-transport or encoding schema. From this viewpoint the BAPI design moves to supporting a north-star of a rich type system [5], [6] that provides a range of Poke-Yoke [7] features to prevent common errors and a language that allows us to provide detailed logical operational constraints on the behavior of the API (2). BAPI extends this specification layer with novel capabilities to express temporal constraints across API uses as well explicit resource access annotations ([sec:bapi,fig:finalapi]). Using this specification language we show how to build a rich ecosystem of tools for mechanized validation of implementations and their usage (3). Finally, we discuss the implications of this design for agentic software development and how it can be used to support safe and effective agentic interactions (4).

2 BAPI Specification Language↩︎

The core of the BAPI is a language that allows us to specify the structure of data in the style of a type system, instead of a data transport schema, which ensures that these specifications can be (type) checked, composed, versioned, just like any other software artifact. In this process we lean into the the ideal of mistake-proofing the specification process [7]. In the domain of hardware design an example of this philosophy is USB-A vs. USB-C, where the symmetrical design of the C connector mistake-proofs the process of connecting a cable. An example in API design is the ability to make an API injection mistake-hardened by providing explicit, and lightweight, syntax for validated string types – type UserID = CString of /[a-zA-Z0-9_]{2, 30}/ – and guaranteeing that the string constraints cannot be used to trigger a denial-of-service attack (ReDOS [8])¹.

From this core system, the next step is to extend the specification language with support for arbitrary logical constraints on the data relations and behavior of the APIs. In BAPI this is done by allowing for invariant declarations on types and pre/post conditions on API operations. However, instead of directly using a dialect of first-order logic, BAPI leverages the Bosque programming language [5].

The Bosque programming language is uniquely well suited for this task as it is specifically designed to support mechanized validation and, as such is fully referentially transparent and deterministic, which eliminate many of the challenges around accidental mutation or flakey behaviors when trying to use a general purpose programming language for specification and runtime validation [10]–[12]. In addition, the Bosque language is designed to map well into the families of logics that are efficiently handled by SMT [13] solvers.

Using this logical specification layer we can improve the payment API example by adding basic sanity check pre/post conditions on the operation.

api transfer(amt: USD, payer: Account, payee: Account)
  requires 0.0<USD> < amt;
  requires amt <= 100.00<USD>;
;

This specification now provides a much safer API, as it prevents the risk of simple fat-finger mistakes or malicious attempts to subvert an AI agent into transferring large amounts of money. In addition this specification also highlights (and prevents) the possible error of using a negative amount for the transfer request. However, this API specification is still unsatisfactory as the upper limit on the transfer amount is hard coded and thus not flexible to changes in the business rules or user needs. This specification is also silent on the possible side-effects of the API operation – for example does it require authorization and access permissions for the payee account, and, is it possible that this API also uploads my account information to hackers.evil.com?

To address these issues BAPI provides two forms of environmental constraints that can be used in the specification language. The first constraint is a set of environment variables that are required for the API to function, such as a PAYMENT_AUTHORIZATION token and the user specified PAYMENT_LIMIT. The second constraint is a set of resource access annotations that specify the resources that the API will access, in this case just the payer’s account information. Explicitly declaring these requirements ensures that a user (human or agent) has the necessary context and also prevents the implementation from accessing any information that is not explicitly provided. Adding these constraints to the API specification we get the following:

api transfer(amt: USD, payer: Account, payee: Account)
  env={
    PAYMENT_AUTHORIZATION: OAUTH_TOKEN,
    PAYMENT_LIMIT: USD
  }
  permissions={
    \account:${payer.routing}/${payer.account}\;
  }

  requires 0.0<USD> < amt;
  requires amt <= env.PAYMENT_LIMIT;
;

The upper bound on the transfer amount is now determined by the user specified PAYMENT_LIMIT environment variable which allows for dynamic adjustment based on the context that this call it made in. In addition, the explicit resource permissions annotation provides a "sandbox" specification for the resources that this API will access. While the idea of sandboxing is well known, the key insight here is using URIs and Globs [14] as the means of resource specification and sandboxing. As opposed to using custom resource types and access languages [15]–[17] which have, historically, been difficult to standardize, understand, and use, URIs and globs naturally match the model of resources used in RESTful systems. This allows for a uniform and natural way to specify and enforce access policies across a wide variety of resource types (files, REST endpoints, databases, etc.) without needing custom plugins or extensions for each type.

These environmental constraints are critical for ensuring that the API is safe to use and that it has the necessary context to function correctly. However, we still lack the critical ability to express temporal constraints on the API operations. For example, that after a blob storage write that a conditional (If-Match) e-tag read will, on success, the read value is the same as previously written, or in the payment API example, that either the payment amount does not exceed a certain limit or that in some previous event we obtained explicit user approval for the operation.

BAPI provides a novel event log system to express temporal constraints on the API operations. This tamper-proof log is a first-class construct in the specification language and allows us to write specifications over the sequence of events that occur during the execution of a system. In contrast to classical temporal logics [18], [19] with limitations on expressiveness or TLA [20] which is not executable, this approach allows developers to express complex temporal constraints on the API operations in a natural and intuitive way.

Each event in the system is recorded in the event log in linear order, and as part of the pre or post conditions of an API operation, this event log is automatically provided via the special variable $events that provides the standard set of List type operations plus special pattern matching query operations. The contains check allows us to determine if, prior to using this API, the system has obtained user approval for the payment operation, even if it exceeds the default payment limit. The final version of the BAPI specification for the payment API is shown in 1.

3 Tooling Ecosystem↩︎

In the vision of a spec-centered development ecosystem, specifications drive the development, testing, and deployment² of the system. The BAPI ecosystem includes high-value tools and workflows that support this vision.

3.1 Automated Test Generation↩︎

Test generation is a critical component of the software development process, and arguably, one of the less desirable and more taxing tasks for developers. However, using the rich type and specification information provided by BAPI, the ability of LLM’s to generate contextually-relevant small values, and the fault-exposing capabilities of combinatorial testing [21] we can generate effective test suites for validating the correctness of implementations and uses of APIs.

The Tecton [22] tool is an automated test generation system that, given only a BAPI specification and (optionally) any existing mock data-sources, generates a comprehensive test suite³. On a set of standard RESTful testing benchmarks [22]–[24] Tecton achieves an effective rate of \(70\%-90\%\) line coverage, comparable to quality human generated suites, and is able to expose between \(2\times\) and \(4\times\) the number of faults as a state-of-the-art white-box fuzzing systems [24]–[26]. Further, given the context (token) efficient nature of BAPI specification and the ability to focus the LLM on compact tasks, these test suites can be generated for under USD \(\$0.10\) in LLM inference cost.

3.2 Automated Validation with Sundew↩︎

In cases where an API implementation or an API client is implemented in the Bosque programming language as well we can go beyond simply testing and apply formal mechanized validation to check that the implementation or use is correct with respect to the specification. As described by the Bosque developers [27], the design of Bosque enables us to map it, almost entirely, to efficiently decidable theories supported by SAT-Module-Theory (SMT) solvers [13]. Operations on numbers, data-types, and functions all map to core decidable theories – Integers, Bitvectors, Constructors, Uninterpreted Functions, and Interpreted Functions. In SMT solvers the theories of Strings and Sequences are semi-decision procedures in the unbounded case.

Sundew performs small-model validation by bounding the sizes of the String and Sequence values, leveraging the small-model hypothesis that the vast majority of errors can be triggered by small (bounded) inputs, and transforming the semi-decision procedure into a fully (and efficiently) decidable system. As a result validation can be fully automated and the result is either (1) a proof that no small input exists that can trigger the error, or (2) a counterexample input that does trigger the error. There is no need for developers to learn an additional proof language, write additional proof lemmas or tactics, or understand the nuances of the underlying logic engine to debug proof failures.

In the case where a full-proof of correctness is desired, it is possible to use standard verification-condition and AI generated inductive invariants [10], [28], [29] to perform modular full-verification of a Bosque program. As Bosque code is the same as the specification logic language this process is applicable to any property that is part of a BAPI specification – or part of an agentic task (4.2).

4 Agentic Coworkers↩︎

The rise of agentic software systems presents a new set of challenges for software development and specification systems have a key role to play in this space. In order for an AI system or Agent to be trustworthy, beyond a statistical guarantee that is "usually does the right thing", we must have a clear and unambiguous specification of the system behaviors it interacts with and the ability to validate its behavior with respect to these requirements. BAPI includes two important features in this space – explicit support for multi-modal specification for AI coding assistants and support for mechanized validation of agentic interactions.

4.1 Multi-Modal Specification for AI Coding Assistants↩︎

Effective specifications for agentic software development need to be multi-modal including natural language, examples, and logical constraints. BAPI specifications, as described in 2, cover all of these modalities except for examples. While, from a theoretical perspective, examples (or test cases) are not strictly necessary, as they can be subsumed by sufficiently strong logical constraints, they are critical in practice for communicating intent concisely when a comprehensive logical specification is difficult to write or understand and can effectively eliminate ambiguity in many cases [30]–[32].

To address this issue BAPI includes an example keyword for declaring example-based specifications that allows developers to provide, inline, a file, or directory of examples that can be used as tests for validating the correctness of an implementation or given to an AI agent as part of the context for generating code. Consider the classic case of an API for a sorting routine that sorts a list of integers. A common mistake in the spec it to only write the postcondition that the output is sorted but neglect to specify that the output must be a permutation of the input! However, even a single example is sufficient to effectively communicate this intent and prevent an LLM from generating a buggy implementation.

function sort(l: List<Int>) -> List<Int>
  example [ 
    List<Int>{3i, 1i, 2i} -> List<Int>{1i, 2i, 3i}
  ];
  ensures $return.isSorted();
;

4.2 Trustworthy AI Agents↩︎

The converse of API implementation is usage, and again the availability of a quality specifications is critical for validating the correctness of an agentic interaction plan (or script). The form of this validation can range from classic runtime-verification of pre/post conditions and invariants [11], [12], which the BAPI specifications are well suited to as they are executable and guaranteed to be side-effect free, to performing a symbolic analysis (using say Sundew) on the interaction script to check that it is correct with respect to the preconditions of all the required API calls.

Consider the example code that takes the contents of msg, determines what “half of the bill” is, and transfers the amount.

action splitBill(msg: String, payee: Account) {
  let amt = agent Chat::compute<Option<USD>>(
    env{}, msg, "What is half of the bill?"
  );

  if(amt === none) {
    return fail("Could not determine amount.");
  }

  api transfer(env{...}, amt, env.account, payee);
  ...
}

This script uses an LLM agent to process the semi-structured text in the payment request msg to determine the amount to pay. If the Chat::compute action were unlucky⁴, or the lunch was particularly expensive, this computed amount could be large enough to exceed the payment limit of the user. However, with the specifications provided for the payment API (1), we can easily catch this at runtime with a precondition failure or statically with symbolic validation. The ability run static validation is a key strength as it can identify possible failures before running the script, which may potentially take destructive actions before being aborted, and it also allows us to provide immediate feedback to the AI agent on possible failures and their causes.

5 Related Work↩︎

The topic of verifiable AI programming has been a focus of research in the formal methods community, with significant work using languages like Lean [28] and Dafny [10] to formally specify and verify the correctness AI generated code. These systems have shown promise in verifying the correctness of AI generated code, but they also demonstrate the limits of existing tooling, particularly in terms of the complexity and size of the specifications required.

Specification and requirements gathering is a major challenge for effective cooperation between human and AI agents in software development. Of particular interest in this space is prior work on multi-modal specification and interaction with End-User Programming [32], [33] systems, such as FlashFill [32] and NLyze [34], and Prorogued Programming [35].

Long-horizon agentic systems and tool use, such as AppWorld [36], LOOP [37] and ToolFormer [38], demonstrates the potential for AI agents to perform complex tasks over extended periods of time. However, these systems also highlight the need for robust failure handling and recovery mechanisms as the unaugmented success rates are at \(70\%\) for simpler tasks but drop off rapidly to the \(45\%\) range for more complex (longer horizon) tasks that involve more complex API (tool) use.

6 Onward!↩︎

This tool paper outlines the Bosque API (BAPI) ecosystem⁵, a software ecosystem designed to support modern spec-centered development and provides examples of high-value tools and workflows that support this vision including automated test generation, support for agentic code generation, and mechanized validation. We believe spec-centered software development, and BAPI, will play a critical role in addressing existing challenges in the software engineering lifecycle as well as emerging security and coding challenges presented by agentic systems.

References↩︎