Alcides Fonseca

What are the measurable outcomes of researchers in the AI world

Alcides Fonseca — Tue, 20 Oct 2026 13:21:55 +0000

Early this month, OpenAI has released several papers answering decades old problems to which mathematicians have dedicated their own careers. This NYT piece on Terrence Tao (who first supported AI when it was AI to help humans in the process of discovery, but shunned them when it became apparent that they were looking for the discovery for discovery sake, and not for the journey of learning.

Personally, I think it's a matter of changing the training dataset to learn in the process, and AI can do maths the human way very soon.

OpenAI has tried to ask for forgiveness by pledging 5 million to mathematics, maybe hoping that they come back in tokens. On the other side of the duopoly, Anthropic has donated shares to the public good, which seems to me impossible to manage.

AI is here to stay, and it's only a matter of us, humans, mathematicians or software developers finding our raison d'être and learning to communicate with AI in a way that it also advances our knowledge.

At the heart of the crisis in the profession is a menacing question. If solving hard problems is a mission of math, what happens when machines can do it faster? So much of higher math — hiring, promotions, graduate training and acclaim — is based on the difficulty, quality and the impact of papers (the written documents explaining proofs) that a mathematician produces.

The consensus is that A.I.-assisted problem solving is the inevitable future, but no one knows exactly what that new world will look like. “Deep uncertainty will persist in these next years,” a draft report by a group of mathematicians meeting at Harvard on Ph.D. education concluded last month.

— Elisabeth Bumiller on Terry Tao Is on the Front Lines of the Debate Over AI and the Future of Math

This is a completely different subject. Academics created a bean counting system to assess progress that is completely fake. Research is a high-risk activity, like Venture Capital. You invest in many different projects and teams, hoping that one out of 100/1000/1 million succeeds and has a huge impact on society. So you should be okay with the losses you take. It's part of the high-risk/high-reward system.

CoARA and Informatics-Europe provide recommendations to assess researchers: focus on the research and forget bean-counting. But even universities that are trying to adopt CoAra (like my employer, U. Lisbon) forget about the goal and come back to KPIs for fear that funding will be given based on KPIs.

Curiosity-driven research has been responsible for many important discoveries and inventions. So there should be a base funding for that. Then, there should be strategic funding for each country's long-term priorities (healthcare, transportation, defense). Meet with people and fund based on the team and the impact that the project might bring.

To assess researchers, let their peers assess them through conversations and presentations about their work. Do not rely on publication counts and other metrics that can be gamed. And if you are not qualified to evaluate a researcher, maybe you shouldn't had hired them in the first place.

Lisbon through the ages

Alcides Fonseca — Tue, 20 Oct 2026 13:10:31 +0000

Lessons learned building Fronteira

Alcides Fonseca — Fri, 16 Oct 2026 12:35:39 +0000

I designed a harness built on top of dependent types that uses information-flow policies to prevent attacks involving the lethal trifecta. However, expecting users to write liquid types was unrealistic, and creating a custom SDK for every external interface—filesystems, APIs, internet search and MCP tools—was not practical.

Following feedback from Lisbon.ai (thanks, Nuno, Fred, Sérgio and David), I started building Fronteira to make these technical ideas accessible to a wider audience.

What is Fronteira?

Fronteira is an MCP proxy that acts as a behavioral firewall. You log in through the browser and add integrations with GitHub, Gmail and other services through their MCP servers. You authenticate your harnesses with Fronteira and automatically get access to all your configured MCP servers. You also get portability across harnesses, but that is just a side effect.

The main advantage of Fronteira is that all MCP interactions go through it, allowing it to track behavior across multiple MCP servers. You get tool-call logging for your harness for free—or, in an enterprise setting, for all your users. I have to admit that this was extremely useful when debugging Fronteira itself, as well as some custom MCP servers.

Because all the data is centralized, we can track where information flows. In particular, this allows Fronteira to stop attacks involving the lethal trifecta. Such an attack can occur when a prompt injection causes an agent to read private data through one tool and expose it to an external endpoint through another. Requiring all interactions to pass through MCP servers is a clear limitation, which I will address later.

Because there are countless MCP providers and possible combinations, each with its own schema, it is impossible for me to write a set of rules that prevents harmful actions for everyone. Instead, Fronteira allows you to write your rules in English and translates them into Guard DSL, a language evaluated deterministically on every interaction.

Users are not expected to write Guard DSL themselves. Instead, they write rules in natural language and can check that the resulting code matches their expectations. The language's usability could be improved, but it is sufficient for the prototypes I have built.

While the rule language is evaluated deterministically, it can invoke nondeterministic components that use decision models—currently JEV—to determine whether content contains trade secrets or medical information. There is also session-level tracking, such as read_private in the example. So far, I have not found anything I could not express, but I am sure that will happen as soon as someone else starts using it.

Limitations and Technical Lessons Learned

The first limitation is clear: top-level harnesses access the filesystem directly, browse the internet directly, control desktop apps and access APIs directly, usually through skills or other instructions. All these interactions bypass Fronteira, making it useless for day-to-day security in your harness.

Second, harnesses come with skills that assume the user is using the harness's official Gmail integration—for example, Codex's integration. If Gmail is only available through Fronteira's MCP endpoint, Codex will sometimes fail to find it out of the box. Deploying Fronteira in the wild would therefore require us to write many skills to change this default behavior.

I also learned that no one respects the fact that MCP tool lists can be dynamic according to the specification. Requests for the tool list can return different results throughout a conversation, but harnesses do not implement support for this. They load the tool list at the beginning and do not reload it unless explicitly asked. I understand the challenge: reloading it before every response would increase the load on MCP servers and add latency. I would like a flag in the response that forces clients to refresh the list.

Furthermore, the MCP schema can change at any time. There is assumption that MCP schemas do not ever change, but I wonder how reliable the assumption is. MCP does not have explicit versioning, although some providers use REST-style versioned endpoints such as /api/v1.

On the other hand, I do not want Fronteira to expose a million tools at all times. I would like it to receive the prompt, or some related information, and dynamically select the relevant tools. Tools forbidden by the rules could then be excluded from the context, rather than occupying space when any attempt to call them would result in an error.

The final technical lesson I learned is that I was too optimistic about trusting Codex with DevOps. I asked it to mirror another app's Django configuration for Fronteira, but it changed the server root, exposing my Resend token and allowing spammers to send spam through my account. The issue was easy to identify and fix, but I expected more from Codex. I also realized that I still do not have a security tool I can point at a deployment, rather than its source code!

Alternatives to Fronteira

I did not look at competitors before implementing Fronteira. This was not because of laziness or incompetence. It was simply not a priority: I wanted to build it regardless, to understand the challenges firsthand.

Behavioral Rules

I was aware of Dogwood, Amazon's temporal specification extension to the Cedar specification (mainly used for AWS access permissions).

Dogwood can require previous explicit approval for some actions. Approval is something I wanted to add to Fronteira from the start through a mobile app. The following temporal rule in Cedar permits a share sale only if the same stock and number of shares were approved within the past hour.

permit (
    principal,
    action == AgentCore::Action::"SellShares",
    resource
)
when temporal {
    formerly within 1h AgentCore::Action::"ApproveSale"::response{
        input.stock: context.input.stock,
        input.shares: context.input.shares,
        output.approved: true
    }
};

To address some of the same limitations as Fronteira, Amazon uses the Dogwood engine in the Strands SDK. By combining the policy engine with a sandbox, they prevent agents from circumventing the "firewall." This is still not foolproof: agents can use a remote browser MCP server to call APIs, avoiding detection.

The Invariant SDK features dataflow guardrails. Both Invariant and Cordon offer MCP proxies like Fronteira. They share the same limitations, but I would like to highlight some interesting language features such as quantifiers and loop detection.

Executor.sh is another MCP proxy that adds some interesting configurations. For instance, it allows you to create policies in typescript, requiring approval of actions, but also more interesting behaviors such as allowing you to undo sending an email in the next 5 minutes.

MCP Proxies with Static Rules

Mintive, previously MintMCP, is very similar to Fronteira, except that it does not support behavioral rules. You can still detect private information leaking through static rules, but you cannot prevent malicious sequences of individually harmless calls.

Both the Lasso Security MCP Gateway and WitnessAI are very similar to Mintive: they automatically manage MCP servers and can detect leaks of information identified as private.

MCP Firewall performs a similar role but also focuses on filtering MCP responses, treating their contents as untrusted because they may contaminate subsequent reasoning.

NVIDIA NeMo is another proxy that validates tool parameters and responses against a range of requirements. However, it does not relate different tool calls to one another except through custom code.

Endram is a proxy that decides whether each call requires manual approval, something Dogwood also supports alongside more complex features.

Both WSO2 and Microsoft Global Secure Access support Cedar-like access control lists for MCP servers, with tool- and prompt-level controls.

Agent Control allows you to create guardrails in Python. These operate at the level of individual tool calls, but Agent Control also integrates with external guardrail infrastructure, such as Dogwood, whose language is more expressive.

Language Specification

AgentSpec is a specification language like Fronteira's, with a more principled design but similar features. I would like to study properties of the language, particularly ways to provide feedback when users write inconsistent rules.

Others

IBM offers MCP ContextForge, a central gateway focused more on discoverability and observability. agentgateway is also mostly focused on observability. TrueFoundry focuses on the M×N problem—M harnesses connecting to N MCP servers—and observability.

LlamaFirewall is similar in that it can inspect traces of calls and detect malicious patterns. However, it does so using a BERT-style LLM, whereas Fronteira primarily supports deterministic analysis.

Comparison Summary

Approach	MCP proxying	Content guards	Behavioral / temporal guards
Fronteira	✅	✅	✅
Dogwood + Strands Box	🚫	✅	✅
Invariant + MCP Scan	✅	✅	✅
Executor.sh	✅	✅	✅
Cordon	✅	🚫	🟡
Mintive / MintMCP	✅	✅	🟡
Lasso MCP Gateway	✅	✅	🚫
WitnessAI	✅	✅	🚫
MCP Firewall	✅	✅	🟡
NVIDIA NeMo Guardrails	🚫	✅	🟡
Endram	✅	🟡	🚫
WSO2 MCP ACL policy	✅	🚫	🚫
Microsoft GSA MCP firewall	✅	🚫	🚫
Agent Control	🚫	✅	🟡
AgentSpec	🚫	🟡	🟡
IBM ContextForge	✅	🟡	🚫
agentgateway	✅	✅	🟡
TrueFoundry	✅	✅	🚫
LlamaFirewall	🚫	✅	✅ (probabilistically)

Conclusion

After this exercise, I no longer believe in MCP proxies as security boundaries for agents. MCP covers only part of an agent's interaction with the world. Another reason is that MCP is a leaky abstraction. Models are post-trained in specific MCP and skill contexts, so they will always prefer direct alternatives, creating friction for the user.

However, I strongly believe in the need for logic-based policies to control agents. Those policies should be enforced at the agent boundary and should probably be developed alongside the harnesses and models. I would love this enforcement to be harness-independent and provided by a third party. However, given how models are becoming increasingly harness-specific, I do not see that working in the long term.

If you have read this far, I am looking for a new opportunity where I can apply my research experience in programming languages, systems and different areas of artificial intelligence to improve the safety of agentic systems. If you are looking for someone with that background, along with the agency and pace of someone who has worked at several startups, you can find my contact details on this website.

If I were a Bank CTO (part 2)

Alcides Fonseca — Thu, 15 Oct 2026 08:03:32 +0000

I certainly would not hire 1,000 third-party consultants to help fix patches. I would probably rethink the architecture of the whole system and company, so that the exposed footprint is minimized. I would give proper training to the internal 3.000 people and power them with AI tooling (even if for monitoring and preventing attacks). And I would even consider open-sourcing the code.

But hiring a lot of (most likely under qualified) people to patch vulnerabilities is a losing game.

The internet was built on hypertext. Now hypertext is a premium feature

Alcides Fonseca — Wed, 14 Oct 2026 17:17:42 +0000

If you subscribe to a Meta One plan, you can add links to a set number of posts and reels each month based on your plan:

Meta One Advanced plan: up to 4 posts and 4 reels with links per month

Meta One Expert plan: up to 8 posts and 8 reels with links per month

Meta One Max plan: up to 12 posts and 12 reels with links per month

Meta is trying to sherlock Linktree. But I can't stop and think it's completely bananas that the internet was built on hypertext and openness, and Instagram created a silo and now it's requiring content creators to pay so their users can have a way out.

AI Models Can Provably Hide Arbitrary Capabilities

Alcides Fonseca — Tue, 13 Oct 2026 12:41:59 +0000

Capability evaluations aim to surface dangerous model behaviors before deploy- ment, but their reliability depends on the assumption that hidden capabilities can be elicited. We show this assumption does not hold under adversarial conditions by constructing backdoor attacks that embed encrypted neural networks within host model weights, decrypting and executing them only upon receiving a secret trigger. Using digital lockers, these hidden circuits remain provably hard to elicit and interpret under cryptographic assumptions, even given full access to model weights, extending prior work from hiding fixed strings to arbitrary computations. We implement our proof of concept constructions in PyTorch and evaluate elicitation through fine-tuning, weight noising, gradient-based trigger search, and latent adversarial training on a small chemical reaction prediction task – a proxy for CBRN-relevant capabilities. Our results demonstrate resistance to these methods and, together with our cryptographic guarantees, reveal a limit of elicitation-based capability audits. We release our models to support the improvement of defenses.

— AI Models Can Provably Hide Arbitrary Capabilities

This paper presents a way for neural networks to hide functionality (encrypted in apparently random weights) until a trigger message is sent.

In the next 007 movie, we see Q writing PyTorch code under pressure from terrorists, maybe Swordfish style.

Paper: Barista - Synthesizing Typestate Specifications with LLM Agents

Alcides Fonseca — Mon, 12 Oct 2026 12:08:23 +0000

This week, we are presenting the Barista paper at ASE'2026, and by 'we', I mean Catarina Gamboa, who is leading this work.

When trying to adopt LiquidJava, an annotation-based language that adds refinements to types, in your Java project, you will have to write the annotations for any library that you use, including the Java Standard Library. This is just a huge amount of work for your simple application. This issue is shared by LiquidHaskell, Frama-C's ACML and Java Modeling Language.

Roughly one year ago, we wanted to explore if we could have LLMs read the documentation (English) and write the specifications for libraries. We focused on a few examples from the Java Standard Library and, given that one year ago LLMs generated more slop than they do today, we came up with an agentic workflow that combined LLM to translate English to an Automata, and the Automata to specification. And by having the automata, we could create positive and negative examples of method call sequences that we could use to validate the generated specification and iterate until we are satisfied.

If you want to learn more about how we come up with the refinements below, you can read the interactive presentation Catarina prepared.

@StateSet({"unconnected", "bound", "connected",
  "inputshutdown", "outputshutdown",
  "bothshutdown", "closed"})
@RefinementAlias("ValidPort(int p) {p >= 0 && p <= 65535}")
@ExternalRefinementsFor("java.net.Socket")
public interface SocketRefinements {

  @StateRefinement(to = "unconnected(this)")
  public void Socket();

  @StateRefinement(to = "connected(this)")
  public void Socket(InetAddress address,
      @Refinement("ValidPort(_)") int port);

  @StateRefinement(from = "unconnected(this)",
                   to = "bound(this)")
  public void bind(SocketAddress bindpoint);

  ...
}

After-thoughts

Presenting this work almost one year after it was conducted feels very strange to me. LLMs have advanced so much in the meantime, that I believe they would be able to get better results without the need for our DFA-oriented architecture. Or probably we would have done a skill-based or tool-based architecture instead of multi-agent. LLMs are now much better at orchestrating the whole process and managing their contextual memory than they were back when we started this.

This paper (along with most of the accepted papers in SE these two years) should probably just be a pre-print, or a living benchmark. The results we present are a product of our time, that would be imperceptible for anyone who wasn't using LLMs to generate code last year, or for the rest of us that forget it easily.

I still see value in our approach, though. I am more and more convinced that we need more verified programming, not to avoid bugs, but rather to gain trust in the source code. While before software engineers would gain trust by building it themselves, and eventually by testing it, both of these tasks are so automated that we need other ways of building trust in our systems. That is an open question that I would love to have a complete answer to. Right now, formal methods and dependently-typed languages are a partial answer to that problem.

If you're in Münich, please go and see Catarina's talk on Thursday.

We need to save Peer Review ourselves

Alcides Fonseca — Sun, 11 Oct 2026 16:21:54 +0000

In our value statements, we usually say we value diversity, but our strategies and plans don’t quite live up that. Academics are themselves diverse. There isn’t a one-size-fits-all job description. The 40-40-20 model itself doesn’t fit everyone, and doesn’t fit every stage of the career. It is natural to focus more on different roles at different times, depending on opportunities and energy. Some of us are just not meant to be president, and not everyone has to lead large EU projects to contribute to research. Individuals sometimes manage to make other types of research contributions by forging productive partnerships, eg between people at different career stages, but it requires them to work against the system a bit, and subvert the expectations the University has written into its metrics.

[...]

Some of my colleagues are probably thinking, based on recent discussions in committees, that I’m kind of bolshie and difficult about university administration activities. Thank you, perhaps yes.

— Being an incentive, being an obstacle, being values by James McDermott

I am the difficult one in my department. Peer Review is in danger, facing an increased number of submissions (both papers and projects for funding). There are AI companies selling solutions to automate some of these solutions, but everyone with a Claude or Codex subscription can generate a paper in a couple of hours. A great paper? maybe not, but enough to be yet another submission to have to review.

In Artificial Intelligence conferences, you are limited to 20 submissions and/or you are required to be a reviewer (ICLR, ICML, NeurIPS). The quality of reviews decreases, and there are undergraduates [reviewing] some papers. I'm all in favor of Shadow PCs, but this seems too random to attribute any level of trust to the reviewers.

In Software Engineering, ICSE defined a maximum of 3 submissions (remember the Guinness World Record-level 12 accepted papers by the same author). ICSE, FSE and TOSEM have also agreed to share review(er)s, to avoid repeated work on the same submissions (reducing the reviewer bias resilience).

Other areas are also following suit with senior authors having to agree to review papers if needed, imposing submission limits, and even adding a submission fee.

These are all patches, not solutions to the problem. Many people have identified the solution: we must not count the number of papers (or funded projects) in the bean-counting process of research evaluation. If you give that much importance to a measure, the measure itself becomes the goal, and Peer Review will not survive.

And who rules the university? We do. It's a collegial management, so we need each of us to rise against these practices. Bureaucrats require KPIs and metrics that do not look at the substance of the work. But the idea of being a collegial organization is that we should look at the substance (and that requires time, that no one wants to spend).

And this is not a new idea. David Parnas said it in 2007, Computing Research Association has said it in 1999 and in 2015.

Another related issue is that when everyone is targeting Q1 and Core A/A* conferences (~top 25% venues), the top 25% conferences are now responsible for 75% of the submissions, and lower ranked venues die. This is non-sensical.

Recommendation R4.1 states: “Publication counts, whether weighted or not, must not be used to evaluate research value.”

— Informatics Europe, Informatics Research Evaluation (2025)

“the scientific content of a paper is much more important than publication metrics or the identity of the journal in which it was published.”

— DORA, recommendation 4

I agree with James, we need to fight for this change ourselves, because the attrition of the big machine of large organizations is against us.

unikernels were hard. key word: were.

Alcides Fonseca — Sat, 10 Oct 2026 23:24:51 +0000

If you deeply care about security, there are really two choices: You're sending satellites into space, and you should probably use seL4, a formally verified operating system. (I'm still a bit salty about the Australian government disbanding that team.) Everyone else should seriously consider unikernels. Stop trying to harden something that is very hackable. Invert it and design from the other direction.

— Geoffrey Huntley in unikernels were hard. key word: were.

I have been a fan of Unikernels since MirageOS was announced, but OCaml was always an issue, mostly because of the lack of libraries for unikernels, but also because of the double semicolon (sorry Jane Streeters, French people and CMUers).

In the age of agents, unikernels make sense to isolate agent tasks so that they have as little (security-attackable) surface as possible, finish as fast as possible, and you can run as many in a single machine as possible.

However, you need some kind of inter-unikernel communication protocol (some lightweight semantic socket) so that you can spawn several unikernels, designed for single-purpose tasks, and gather the results they found.

If you are working on such a topic, hit me up.

Is sandboxing sufficient to contain rogue agents? – A Few Thoughts on Cryptographic Engineering

Alcides Fonseca — Fri, 09 Oct 2026 17:36:51 +0000

Unfortunately, monitoring for adversarial data access turns out to be one of the hardest problems you could imagine. The volume of data that agents produce is so high that no human being could possibly read it, and we probably wouldn’t recognize obfuscated malicious data even if we were looking directly at it. This means any attempt to monitor the inflow/outflow will have to be handled by other models. Thus, the future of agent sandboxing is (1) build a sandbox, (2) install an agent/model into it, (3) install a somewhat dumber/cheaper warden model to guard it, (4) hope you can trust the lunkhead to contain the wizard. And so on and so forth, as models become more intelligent and capable.

In other words: a warden-guarded sandbox is just another version of the alignment problem. You’re going to have to trust a model to do it, and that model will need to be at least some fraction as intelligent as the model it’s guarding. If you haven’t convinced yourself that it’s possible to build models you can trust, then sandboxing isn’t going to take you much farther.

— Matthew Green in Is sandboxing sufficient to contain rogue agents? – A Few Thoughts on Cryptographic Engineering

Matthew Green, a cryptographer at Johns Hopkins University, points out what I have been saying for a while: if you want your agents to be useful, they have to be able to access information and perform actions. How do you prevent those actions from being harmful? You use another agent to deny or allow each action. Thus alignment is still relevant, even if for the bouncer controlling the sandbox escape.

I actually believe we should be using deterministic guardrails that can be audited, instead of another model as a border patrol agent. I am working on such solution, which I will be sharing soon enough.